YES 3.206
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ CR
mainModule Main
|
| ((max :: (Ord b, Ord a) => Either a b -> Either a b -> Either a b) :: (Ord a, Ord b) => Either a b -> Either a b -> Either a b) |
module Main where
Case Reductions:
The following Case expression
| case | compare x y of |
| | EQ | → o |
| | LT | → LT |
| | GT | → GT |
is transformed to
| primCompAux0 | o EQ | = o |
| primCompAux0 | o LT | = LT |
| primCompAux0 | o GT | = GT |
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
mainModule Main
|
| ((max :: (Ord a, Ord b) => Either b a -> Either b a -> Either b a) :: (Ord a, Ord b) => Either b a -> Either b a -> Either b a) |
module Main where
If Reductions:
The following If expression
if primGEqNatS x y then Succ (primDivNatS (primMinusNatS x y) (Succ y)) else Zero
is transformed to
| primDivNatS0 | x y True | = Succ (primDivNatS (primMinusNatS x y) (Succ y)) |
| primDivNatS0 | x y False | = Zero |
The following If expression
if primGEqNatS x y then primModNatS (primMinusNatS x y) (Succ y) else Succ x
is transformed to
| primModNatS0 | x y True | = primModNatS (primMinusNatS x y) (Succ y) |
| primModNatS0 | x y False | = Succ x |
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
mainModule Main
|
| ((max :: (Ord a, Ord b) => Either a b -> Either a b -> Either a b) :: (Ord b, Ord a) => Either a b -> Either a b -> Either a b) |
module Main where
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule Main
|
| ((max :: (Ord b, Ord a) => Either a b -> Either a b -> Either a b) :: (Ord b, Ord a) => Either a b -> Either a b -> Either a b) |
module Main where
Cond Reductions:
The following Function with conditions
| compare | x y |
| | | x == y | |
| | | x <= y | |
| | | otherwise | |
|
is transformed to
| compare | x y | = compare3 x y |
| compare2 | x y True | = EQ |
| compare2 | x y False | = compare1 x y (x <= y) |
| compare1 | x y True | = LT |
| compare1 | x y False | = compare0 x y otherwise |
| compare3 | x y | = compare2 x y (x == y) |
The following Function with conditions
is transformed to
| max1 | x y True | = y |
| max1 | x y False | = max0 x y otherwise |
| max2 | x y | = max1 x y (x <= y) |
The following Function with conditions
| gcd' | x 0 | = x |
| gcd' | x y | = gcd' y (x `rem` y) |
is transformed to
| gcd' | x zx | = gcd'2 x zx |
| gcd' | x y | = gcd'0 x y |
| gcd'0 | x y | = gcd' y (x `rem` y) |
| gcd'1 | True x zx | = x |
| gcd'1 | zy zz vuu | = gcd'0 zz vuu |
| gcd'2 | x zx | = gcd'1 (zx == 0) x zx |
| gcd'2 | vuv vuw | = gcd'0 vuv vuw |
The following Function with conditions
| gcd | 0 0 | = error [] |
| gcd | x y | =
| gcd' (abs x) (abs y) |
| where |
| gcd' | x 0 | = x |
| gcd' | x y | = gcd' y (x `rem` y) |
|
|
is transformed to
| gcd | vux vuy | = gcd3 vux vuy |
| gcd | x y | = gcd0 x y |
| gcd0 | x y | =
| gcd' (abs x) (abs y) |
| where |
| gcd' | x zx | = gcd'2 x zx |
| gcd' | x y | = gcd'0 x y |
|
|
| gcd'0 | x y | = gcd' y (x `rem` y) |
|
|
| gcd'1 | True x zx | = x |
| gcd'1 | zy zz vuu | = gcd'0 zz vuu |
|
|
| gcd'2 | x zx | = gcd'1 (zx == 0) x zx |
| gcd'2 | vuv vuw | = gcd'0 vuv vuw |
|
|
| gcd1 | True vux vuy | = error [] |
| gcd1 | vuz vvu vvv | = gcd0 vvu vvv |
| gcd2 | True vux vuy | = gcd1 (vuy == 0) vux vuy |
| gcd2 | vvw vvx vvy | = gcd0 vvx vvy |
| gcd3 | vux vuy | = gcd2 (vux == 0) vux vuy |
| gcd3 | vvz vwu | = gcd0 vvz vwu |
The following Function with conditions
is transformed to
| absReal0 | x True | = `negate` x |
| absReal1 | x True | = x |
| absReal1 | x False | = absReal0 x otherwise |
| absReal2 | x | = absReal1 x (x >= 0) |
The following Function with conditions
is transformed to
| undefined0 | True | = undefined |
| undefined1 | | = undefined0 False |
The following Function with conditions
| reduce | x y |
| | | y == 0 | |
| | | otherwise |
| = | x `quot` d :% (y `quot` d) |
|
|
| where | |
|
is transformed to
| reduce2 | x y | =
| reduce1 x y (y == 0) |
| where | |
|
| reduce0 | x y True | = x `quot` d :% (y `quot` d) |
|
|
| reduce1 | x y True | = error [] |
| reduce1 | x y False | = reduce0 x y otherwise |
|
|
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
mainModule Main
|
| ((max :: (Ord a, Ord b) => Either b a -> Either b a -> Either b a) :: (Ord b, Ord a) => Either b a -> Either b a -> Either b a) |
module Main where
Let/Where Reductions:
The bindings of the following Let/Where expression
| reduce1 x y (y == 0) |
| where | |
|
| reduce0 | x y True | = x `quot` d :% (y `quot` d) |
|
|
| reduce1 | x y True | = error [] |
| reduce1 | x y False | = reduce0 x y otherwise |
|
are unpacked to the following functions on top level
| reduce2Reduce1 | vwv vww x y True | = error [] |
| reduce2Reduce1 | vwv vww x y False | = reduce2Reduce0 vwv vww x y otherwise |
| reduce2Reduce0 | vwv vww x y True | = x `quot` reduce2D vwv vww :% (y `quot` reduce2D vwv vww) |
| reduce2D | vwv vww | = gcd vwv vww |
The bindings of the following Let/Where expression
| gcd' (abs x) (abs y) |
| where |
| gcd' | x zx | = gcd'2 x zx |
| gcd' | x y | = gcd'0 x y |
|
|
| gcd'0 | x y | = gcd' y (x `rem` y) |
|
|
| gcd'1 | True x zx | = x |
| gcd'1 | zy zz vuu | = gcd'0 zz vuu |
|
|
| gcd'2 | x zx | = gcd'1 (zx == 0) x zx |
| gcd'2 | vuv vuw | = gcd'0 vuv vuw |
|
are unpacked to the following functions on top level
| gcd0Gcd'2 | x zx | = gcd0Gcd'1 (zx == 0) x zx |
| gcd0Gcd'2 | vuv vuw | = gcd0Gcd'0 vuv vuw |
| gcd0Gcd' | x zx | = gcd0Gcd'2 x zx |
| gcd0Gcd' | x y | = gcd0Gcd'0 x y |
| gcd0Gcd'1 | True x zx | = x |
| gcd0Gcd'1 | zy zz vuu | = gcd0Gcd'0 zz vuu |
| gcd0Gcd'0 | x y | = gcd0Gcd' y (x `rem` y) |
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
mainModule Main
|
| ((max :: (Ord b, Ord a) => Either b a -> Either b a -> Either b a) :: (Ord b, Ord a) => Either b a -> Either b a -> Either b a) |
module Main where
Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
mainModule Main
|
| (max :: (Ord b, Ord a) => Either b a -> Either b a -> Either b a) |
module Main where
Haskell To QDPs
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primEqNat(Succ(vwx3700), Succ(vwx3800)) → new_primEqNat(vwx3700, vwx3800)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primEqNat(Succ(vwx3700), Succ(vwx3800)) → new_primEqNat(vwx3700, vwx3800)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusNat(Succ(vwx6700), Succ(vwx301000)) → new_primPlusNat(vwx6700, vwx301000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusNat(Succ(vwx6700), Succ(vwx301000)) → new_primPlusNat(vwx6700, vwx301000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primMulNat(Succ(vwx40000), Succ(vwx30100)) → new_primMulNat(vwx40000, Succ(vwx30100))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMulNat(Succ(vwx40000), Succ(vwx30100)) → new_primMulNat(vwx40000, Succ(vwx30100))
The graph contains the following edges 1 > 1, 2 >= 2
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_esEs3(@3(vwx370, vwx371, vwx372), @3(vwx380, vwx381, vwx382), baf, app(app(ty_@2, bcd), bce), bcc) → new_esEs1(vwx371, vwx381, bcd, bce)
new_esEs3(@3(vwx370, vwx371, vwx372), @3(vwx380, vwx381, vwx382), baf, app(ty_Maybe, bcg), bcc) → new_esEs2(vwx371, vwx381, bcg)
new_esEs0(Left(vwx370), Left(vwx380), app(ty_[], da), ce) → new_esEs(vwx370, vwx380, da)
new_esEs2(Just(vwx370), Just(vwx380), app(ty_[], baa)) → new_esEs(vwx370, vwx380, baa)
new_esEs1(@2(vwx370, vwx371), @2(vwx380, vwx381), eh, app(app(app(ty_@3, fh), ga), gb)) → new_esEs3(vwx371, vwx381, fh, ga, gb)
new_esEs3(@3(vwx370, vwx371, vwx372), @3(vwx380, vwx381, vwx382), baf, bag, app(app(app(ty_@3, bbf), bbg), bbh)) → new_esEs3(vwx372, vwx382, bbf, bbg, bbh)
new_esEs3(@3(vwx370, vwx371, vwx372), @3(vwx380, vwx381, vwx382), baf, bag, app(ty_[], bbd)) → new_esEs(vwx372, vwx382, bbd)
new_esEs1(@2(vwx370, vwx371), @2(vwx380, vwx381), app(app(ty_Either, gc), gd), ge) → new_esEs0(vwx370, vwx380, gc, gd)
new_esEs1(@2(vwx370, vwx371), @2(vwx380, vwx381), eh, app(app(ty_Either, fa), fb)) → new_esEs0(vwx371, vwx381, fa, fb)
new_esEs3(@3(vwx370, vwx371, vwx372), @3(vwx380, vwx381, vwx382), app(app(ty_@2, bde), bdf), bag, bcc) → new_esEs1(vwx370, vwx380, bde, bdf)
new_esEs(:(vwx370, vwx371), :(vwx380, vwx381), app(app(app(ty_@3, bh), ca), cb)) → new_esEs3(vwx370, vwx380, bh, ca, cb)
new_esEs0(Right(vwx370), Right(vwx380), df, app(app(ty_@2, ea), eb)) → new_esEs1(vwx370, vwx380, ea, eb)
new_esEs3(@3(vwx370, vwx371, vwx372), @3(vwx380, vwx381, vwx382), app(ty_[], bdg), bag, bcc) → new_esEs(vwx370, vwx380, bdg)
new_esEs3(@3(vwx370, vwx371, vwx372), @3(vwx380, vwx381, vwx382), baf, app(ty_[], bcf), bcc) → new_esEs(vwx371, vwx381, bcf)
new_esEs0(Left(vwx370), Left(vwx380), app(app(app(ty_@3, dc), dd), de), ce) → new_esEs3(vwx370, vwx380, dc, dd, de)
new_esEs2(Just(vwx370), Just(vwx380), app(ty_Maybe, bab)) → new_esEs2(vwx370, vwx380, bab)
new_esEs0(Left(vwx370), Left(vwx380), app(app(ty_Either, cc), cd), ce) → new_esEs0(vwx370, vwx380, cc, cd)
new_esEs2(Just(vwx370), Just(vwx380), app(app(ty_@2, hg), hh)) → new_esEs1(vwx370, vwx380, hg, hh)
new_esEs1(@2(vwx370, vwx371), @2(vwx380, vwx381), eh, app(ty_[], ff)) → new_esEs(vwx371, vwx381, ff)
new_esEs(:(vwx370, vwx371), :(vwx380, vwx381), app(ty_Maybe, bg)) → new_esEs2(vwx370, vwx380, bg)
new_esEs1(@2(vwx370, vwx371), @2(vwx380, vwx381), app(ty_Maybe, ha), ge) → new_esEs2(vwx370, vwx380, ha)
new_esEs0(Right(vwx370), Right(vwx380), df, app(app(app(ty_@3, ee), ef), eg)) → new_esEs3(vwx370, vwx380, ee, ef, eg)
new_esEs1(@2(vwx370, vwx371), @2(vwx380, vwx381), app(ty_[], gh), ge) → new_esEs(vwx370, vwx380, gh)
new_esEs0(Right(vwx370), Right(vwx380), df, app(app(ty_Either, dg), dh)) → new_esEs0(vwx370, vwx380, dg, dh)
new_esEs0(Left(vwx370), Left(vwx380), app(ty_Maybe, db), ce) → new_esEs2(vwx370, vwx380, db)
new_esEs0(Right(vwx370), Right(vwx380), df, app(ty_Maybe, ed)) → new_esEs2(vwx370, vwx380, ed)
new_esEs1(@2(vwx370, vwx371), @2(vwx380, vwx381), eh, app(app(ty_@2, fc), fd)) → new_esEs1(vwx371, vwx381, fc, fd)
new_esEs(:(vwx370, vwx371), :(vwx380, vwx381), app(app(ty_@2, bd), be)) → new_esEs1(vwx370, vwx380, bd, be)
new_esEs3(@3(vwx370, vwx371, vwx372), @3(vwx380, vwx381, vwx382), baf, app(app(app(ty_@3, bch), bda), bdb), bcc) → new_esEs3(vwx371, vwx381, bch, bda, bdb)
new_esEs(:(vwx370, vwx371), :(vwx380, vwx381), app(app(ty_Either, bb), bc)) → new_esEs0(vwx370, vwx380, bb, bc)
new_esEs(:(vwx370, vwx371), :(vwx380, vwx381), ba) → new_esEs(vwx371, vwx381, ba)
new_esEs3(@3(vwx370, vwx371, vwx372), @3(vwx380, vwx381, vwx382), baf, bag, app(app(ty_@2, bbb), bbc)) → new_esEs1(vwx372, vwx382, bbb, bbc)
new_esEs1(@2(vwx370, vwx371), @2(vwx380, vwx381), app(app(app(ty_@3, hb), hc), hd), ge) → new_esEs3(vwx370, vwx380, hb, hc, hd)
new_esEs1(@2(vwx370, vwx371), @2(vwx380, vwx381), app(app(ty_@2, gf), gg), ge) → new_esEs1(vwx370, vwx380, gf, gg)
new_esEs3(@3(vwx370, vwx371, vwx372), @3(vwx380, vwx381, vwx382), baf, bag, app(ty_Maybe, bbe)) → new_esEs2(vwx372, vwx382, bbe)
new_esEs3(@3(vwx370, vwx371, vwx372), @3(vwx380, vwx381, vwx382), app(ty_Maybe, bdh), bag, bcc) → new_esEs2(vwx370, vwx380, bdh)
new_esEs0(Right(vwx370), Right(vwx380), df, app(ty_[], ec)) → new_esEs(vwx370, vwx380, ec)
new_esEs1(@2(vwx370, vwx371), @2(vwx380, vwx381), eh, app(ty_Maybe, fg)) → new_esEs2(vwx371, vwx381, fg)
new_esEs2(Just(vwx370), Just(vwx380), app(app(ty_Either, he), hf)) → new_esEs0(vwx370, vwx380, he, hf)
new_esEs2(Just(vwx370), Just(vwx380), app(app(app(ty_@3, bac), bad), bae)) → new_esEs3(vwx370, vwx380, bac, bad, bae)
new_esEs3(@3(vwx370, vwx371, vwx372), @3(vwx380, vwx381, vwx382), baf, app(app(ty_Either, bca), bcb), bcc) → new_esEs0(vwx371, vwx381, bca, bcb)
new_esEs3(@3(vwx370, vwx371, vwx372), @3(vwx380, vwx381, vwx382), baf, bag, app(app(ty_Either, bah), bba)) → new_esEs0(vwx372, vwx382, bah, bba)
new_esEs(:(vwx370, vwx371), :(vwx380, vwx381), app(ty_[], bf)) → new_esEs(vwx370, vwx380, bf)
new_esEs3(@3(vwx370, vwx371, vwx372), @3(vwx380, vwx381, vwx382), app(app(app(ty_@3, bea), beb), bec), bag, bcc) → new_esEs3(vwx370, vwx380, bea, beb, bec)
new_esEs0(Left(vwx370), Left(vwx380), app(app(ty_@2, cf), cg), ce) → new_esEs1(vwx370, vwx380, cf, cg)
new_esEs3(@3(vwx370, vwx371, vwx372), @3(vwx380, vwx381, vwx382), app(app(ty_Either, bdc), bdd), bag, bcc) → new_esEs0(vwx370, vwx380, bdc, bdd)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_esEs2(Just(vwx370), Just(vwx380), app(app(app(ty_@3, bac), bad), bae)) → new_esEs3(vwx370, vwx380, bac, bad, bae)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(Just(vwx370), Just(vwx380), app(app(ty_Either, he), hf)) → new_esEs0(vwx370, vwx380, he, hf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(vwx370, vwx371), :(vwx380, vwx381), app(app(app(ty_@3, bh), ca), cb)) → new_esEs3(vwx370, vwx380, bh, ca, cb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(:(vwx370, vwx371), :(vwx380, vwx381), app(app(ty_Either, bb), bc)) → new_esEs0(vwx370, vwx380, bb, bc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Just(vwx370), Just(vwx380), app(ty_Maybe, bab)) → new_esEs2(vwx370, vwx380, bab)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(vwx370, vwx371), :(vwx380, vwx381), app(ty_Maybe, bg)) → new_esEs2(vwx370, vwx380, bg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Just(vwx370), Just(vwx380), app(app(ty_@2, hg), hh)) → new_esEs1(vwx370, vwx380, hg, hh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Just(vwx370), Just(vwx380), app(ty_[], baa)) → new_esEs(vwx370, vwx380, baa)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(vwx370, vwx371), :(vwx380, vwx381), app(app(ty_@2, bd), be)) → new_esEs1(vwx370, vwx380, bd, be)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(@2(vwx370, vwx371), @2(vwx380, vwx381), eh, app(app(app(ty_@3, fh), ga), gb)) → new_esEs3(vwx371, vwx381, fh, ga, gb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs1(@2(vwx370, vwx371), @2(vwx380, vwx381), app(app(app(ty_@3, hb), hc), hd), ge) → new_esEs3(vwx370, vwx380, hb, hc, hd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs3(@3(vwx370, vwx371, vwx372), @3(vwx380, vwx381, vwx382), baf, bag, app(app(app(ty_@3, bbf), bbg), bbh)) → new_esEs3(vwx372, vwx382, bbf, bbg, bbh)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_esEs3(@3(vwx370, vwx371, vwx372), @3(vwx380, vwx381, vwx382), baf, app(app(app(ty_@3, bch), bda), bdb), bcc) → new_esEs3(vwx371, vwx381, bch, bda, bdb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs3(@3(vwx370, vwx371, vwx372), @3(vwx380, vwx381, vwx382), app(app(app(ty_@3, bea), beb), bec), bag, bcc) → new_esEs3(vwx370, vwx380, bea, beb, bec)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(Left(vwx370), Left(vwx380), app(app(app(ty_@3, dc), dd), de), ce) → new_esEs3(vwx370, vwx380, dc, dd, de)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(Right(vwx370), Right(vwx380), df, app(app(app(ty_@3, ee), ef), eg)) → new_esEs3(vwx370, vwx380, ee, ef, eg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs1(@2(vwx370, vwx371), @2(vwx380, vwx381), app(app(ty_Either, gc), gd), ge) → new_esEs0(vwx370, vwx380, gc, gd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(@2(vwx370, vwx371), @2(vwx380, vwx381), eh, app(app(ty_Either, fa), fb)) → new_esEs0(vwx371, vwx381, fa, fb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(@2(vwx370, vwx371), @2(vwx380, vwx381), app(ty_Maybe, ha), ge) → new_esEs2(vwx370, vwx380, ha)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(@2(vwx370, vwx371), @2(vwx380, vwx381), eh, app(ty_Maybe, fg)) → new_esEs2(vwx371, vwx381, fg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(@2(vwx370, vwx371), @2(vwx380, vwx381), eh, app(app(ty_@2, fc), fd)) → new_esEs1(vwx371, vwx381, fc, fd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(@2(vwx370, vwx371), @2(vwx380, vwx381), app(app(ty_@2, gf), gg), ge) → new_esEs1(vwx370, vwx380, gf, gg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(@2(vwx370, vwx371), @2(vwx380, vwx381), eh, app(ty_[], ff)) → new_esEs(vwx371, vwx381, ff)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(@2(vwx370, vwx371), @2(vwx380, vwx381), app(ty_[], gh), ge) → new_esEs(vwx370, vwx380, gh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(vwx370, vwx371), :(vwx380, vwx381), ba) → new_esEs(vwx371, vwx381, ba)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
- new_esEs(:(vwx370, vwx371), :(vwx380, vwx381), app(ty_[], bf)) → new_esEs(vwx370, vwx380, bf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(@3(vwx370, vwx371, vwx372), @3(vwx380, vwx381, vwx382), baf, app(app(ty_Either, bca), bcb), bcc) → new_esEs0(vwx371, vwx381, bca, bcb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(@3(vwx370, vwx371, vwx372), @3(vwx380, vwx381, vwx382), baf, bag, app(app(ty_Either, bah), bba)) → new_esEs0(vwx372, vwx382, bah, bba)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs3(@3(vwx370, vwx371, vwx372), @3(vwx380, vwx381, vwx382), app(app(ty_Either, bdc), bdd), bag, bcc) → new_esEs0(vwx370, vwx380, bdc, bdd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(Left(vwx370), Left(vwx380), app(app(ty_Either, cc), cd), ce) → new_esEs0(vwx370, vwx380, cc, cd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(Right(vwx370), Right(vwx380), df, app(app(ty_Either, dg), dh)) → new_esEs0(vwx370, vwx380, dg, dh)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(@3(vwx370, vwx371, vwx372), @3(vwx380, vwx381, vwx382), baf, app(ty_Maybe, bcg), bcc) → new_esEs2(vwx371, vwx381, bcg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(@3(vwx370, vwx371, vwx372), @3(vwx380, vwx381, vwx382), app(ty_Maybe, bdh), bag, bcc) → new_esEs2(vwx370, vwx380, bdh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(@3(vwx370, vwx371, vwx372), @3(vwx380, vwx381, vwx382), baf, bag, app(ty_Maybe, bbe)) → new_esEs2(vwx372, vwx382, bbe)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs0(Left(vwx370), Left(vwx380), app(ty_Maybe, db), ce) → new_esEs2(vwx370, vwx380, db)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(Right(vwx370), Right(vwx380), df, app(ty_Maybe, ed)) → new_esEs2(vwx370, vwx380, ed)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(@3(vwx370, vwx371, vwx372), @3(vwx380, vwx381, vwx382), baf, app(app(ty_@2, bcd), bce), bcc) → new_esEs1(vwx371, vwx381, bcd, bce)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(@3(vwx370, vwx371, vwx372), @3(vwx380, vwx381, vwx382), app(app(ty_@2, bde), bdf), bag, bcc) → new_esEs1(vwx370, vwx380, bde, bdf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(@3(vwx370, vwx371, vwx372), @3(vwx380, vwx381, vwx382), baf, bag, app(app(ty_@2, bbb), bbc)) → new_esEs1(vwx372, vwx382, bbb, bbc)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs3(@3(vwx370, vwx371, vwx372), @3(vwx380, vwx381, vwx382), baf, bag, app(ty_[], bbd)) → new_esEs(vwx372, vwx382, bbd)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs3(@3(vwx370, vwx371, vwx372), @3(vwx380, vwx381, vwx382), app(ty_[], bdg), bag, bcc) → new_esEs(vwx370, vwx380, bdg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(@3(vwx370, vwx371, vwx372), @3(vwx380, vwx381, vwx382), baf, app(ty_[], bcf), bcc) → new_esEs(vwx371, vwx381, bcf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs0(Right(vwx370), Right(vwx380), df, app(app(ty_@2, ea), eb)) → new_esEs1(vwx370, vwx380, ea, eb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs0(Left(vwx370), Left(vwx380), app(app(ty_@2, cf), cg), ce) → new_esEs1(vwx370, vwx380, cf, cg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(Left(vwx370), Left(vwx380), app(ty_[], da), ce) → new_esEs(vwx370, vwx380, da)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(Right(vwx370), Right(vwx380), df, app(ty_[], ec)) → new_esEs(vwx370, vwx380, ec)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primCmpNat(Succ(vwx3000), Succ(vwx4000)) → new_primCmpNat(vwx3000, vwx4000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primCmpNat(Succ(vwx3000), Succ(vwx4000)) → new_primCmpNat(vwx3000, vwx4000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_ltEs(@2(vwx300, vwx301), @2(vwx400, vwx401), app(ty_Maybe, cf), ce) → new_compare20(vwx300, vwx400, new_esEs5(vwx300, vwx400, cf), cf)
new_lt(vwx300, vwx400, cc, cd) → new_compare2(vwx300, vwx400, new_esEs4(vwx300, vwx400, cc, cd), cc, cd)
new_ltEs0(Just(vwx300), Just(vwx400), app(app(app(ty_@3, ed), ee), ef)) → new_ltEs3(vwx300, vwx400, ed, ee, ef)
new_ltEs3(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), baf, app(ty_Maybe, bcd), bcc) → new_lt0(vwx301, vwx401, bcd)
new_ltEs3(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), baf, app(app(ty_Either, bce), bcf), bcc) → new_lt1(vwx301, vwx401, bce, bcf)
new_compare2(vwx300, vwx400, False, cc, cd) → new_ltEs(vwx300, vwx400, cc, cd)
new_ltEs1(Left(vwx300), Left(vwx400), app(app(ty_Either, fc), fd), fa) → new_ltEs1(vwx300, vwx400, fc, fd)
new_ltEs1(Left(vwx300), Left(vwx400), app(ty_Maybe, fb), fa) → new_ltEs0(vwx300, vwx400, fb)
new_compare5(vwx300, vwx400, dc, dd, de) → new_compare22(vwx300, vwx400, new_esEs7(vwx300, vwx400, dc, dd, de), dc, dd, de)
new_compare3(vwx300, vwx400, cf) → new_compare20(vwx300, vwx400, new_esEs5(vwx300, vwx400, cf), cf)
new_ltEs1(Right(vwx300), Right(vwx400), gb, app(app(app(ty_@3, ha), hb), hc)) → new_ltEs3(vwx300, vwx400, ha, hb, hc)
new_ltEs3(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), baf, app(ty_[], bcg), bcc) → new_lt2(vwx301, vwx401, bcg)
new_ltEs1(Left(vwx300), Left(vwx400), app(app(ty_@2, eg), eh), fa) → new_ltEs(vwx300, vwx400, eg, eh)
new_ltEs3(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), app(app(ty_@2, bdc), bdd), bag, bcc) → new_lt(vwx300, vwx400, bdc, bdd)
new_ltEs3(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), app(ty_[], bdh), bag, bcc) → new_lt2(vwx300, vwx400, bdh)
new_ltEs1(Left(vwx300), Left(vwx400), app(ty_[], ff), fa) → new_ltEs2(vwx300, vwx400, ff)
new_ltEs0(Just(vwx300), Just(vwx400), app(ty_Maybe, dh)) → new_ltEs0(vwx300, vwx400, dh)
new_compare22(vwx300, vwx400, False, dc, dd, de) → new_ltEs3(vwx300, vwx400, dc, dd, de)
new_ltEs3(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), app(app(ty_Either, bdf), bdg), bag, bcc) → new_lt1(vwx300, vwx400, bdf, bdg)
new_ltEs3(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), baf, bag, app(ty_Maybe, bbb)) → new_ltEs0(vwx302, vwx402, bbb)
new_ltEs3(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), baf, bag, app(ty_[], bbe)) → new_ltEs2(vwx302, vwx402, bbe)
new_primCompAux(vwx300, vwx400, vwx49, app(ty_[], bab)) → new_compare(vwx300, vwx400, bab)
new_ltEs(@2(vwx300, vwx301), @2(vwx400, vwx401), app(ty_[], db), ce) → new_compare(vwx300, vwx400, db)
new_ltEs1(Right(vwx300), Right(vwx400), gb, app(app(ty_@2, gc), gd)) → new_ltEs(vwx300, vwx400, gc, gd)
new_lt3(vwx300, vwx400, dc, dd, de) → new_compare22(vwx300, vwx400, new_esEs7(vwx300, vwx400, dc, dd, de), dc, dd, de)
new_compare21(vwx300, vwx400, False, cg, da) → new_ltEs1(vwx300, vwx400, cg, da)
new_ltEs1(Right(vwx300), Right(vwx400), gb, app(ty_Maybe, ge)) → new_ltEs0(vwx300, vwx400, ge)
new_ltEs2(:(vwx300, vwx301), :(vwx400, vwx401), hd) → new_primCompAux(vwx300, vwx400, new_compare0(vwx301, vwx401, hd), hd)
new_primCompAux(vwx300, vwx400, vwx49, app(app(ty_Either, hh), baa)) → new_compare4(vwx300, vwx400, hh, baa)
new_ltEs(@2(vwx300, vwx301), @2(vwx400, vwx401), ba, app(app(app(ty_@3, bh), ca), cb)) → new_ltEs3(vwx301, vwx401, bh, ca, cb)
new_lt1(vwx300, vwx400, cg, da) → new_compare21(vwx300, vwx400, new_esEs6(vwx300, vwx400, cg, da), cg, da)
new_ltEs1(Right(vwx300), Right(vwx400), gb, app(ty_[], gh)) → new_ltEs2(vwx300, vwx400, gh)
new_ltEs3(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), baf, bag, app(app(ty_@2, bah), bba)) → new_ltEs(vwx302, vwx402, bah, bba)
new_ltEs3(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), baf, app(app(ty_@2, bca), bcb), bcc) → new_lt(vwx301, vwx401, bca, bcb)
new_ltEs3(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), baf, bag, app(app(app(ty_@3, bbf), bbg), bbh)) → new_ltEs3(vwx302, vwx402, bbf, bbg, bbh)
new_primCompAux(vwx300, vwx400, vwx49, app(app(app(ty_@3, bac), bad), bae)) → new_compare5(vwx300, vwx400, bac, bad, bae)
new_ltEs2(:(vwx300, vwx301), :(vwx400, vwx401), hd) → new_compare(vwx301, vwx401, hd)
new_ltEs3(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), app(app(app(ty_@3, bea), beb), bec), bag, bcc) → new_lt3(vwx300, vwx400, bea, beb, bec)
new_ltEs0(Just(vwx300), Just(vwx400), app(ty_[], ec)) → new_ltEs2(vwx300, vwx400, ec)
new_compare(:(vwx300, vwx301), :(vwx400, vwx401), hd) → new_compare(vwx301, vwx401, hd)
new_ltEs3(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), baf, bag, app(app(ty_Either, bbc), bbd)) → new_ltEs1(vwx302, vwx402, bbc, bbd)
new_ltEs0(Just(vwx300), Just(vwx400), app(app(ty_@2, df), dg)) → new_ltEs(vwx300, vwx400, df, dg)
new_ltEs0(Just(vwx300), Just(vwx400), app(app(ty_Either, ea), eb)) → new_ltEs1(vwx300, vwx400, ea, eb)
new_compare(:(vwx300, vwx301), :(vwx400, vwx401), hd) → new_primCompAux(vwx300, vwx400, new_compare0(vwx301, vwx401, hd), hd)
new_ltEs(@2(vwx300, vwx301), @2(vwx400, vwx401), ba, app(app(ty_@2, bb), bc)) → new_ltEs(vwx301, vwx401, bb, bc)
new_ltEs(@2(vwx300, vwx301), @2(vwx400, vwx401), app(app(ty_Either, cg), da), ce) → new_compare21(vwx300, vwx400, new_esEs6(vwx300, vwx400, cg, da), cg, da)
new_ltEs1(Right(vwx300), Right(vwx400), gb, app(app(ty_Either, gf), gg)) → new_ltEs1(vwx300, vwx400, gf, gg)
new_ltEs3(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), baf, app(app(app(ty_@3, bch), bda), bdb), bcc) → new_lt3(vwx301, vwx401, bch, bda, bdb)
new_ltEs(@2(vwx300, vwx301), @2(vwx400, vwx401), ba, app(ty_[], bg)) → new_ltEs2(vwx301, vwx401, bg)
new_lt2(vwx300, vwx400, db) → new_compare(vwx300, vwx400, db)
new_ltEs(@2(vwx300, vwx301), @2(vwx400, vwx401), ba, app(ty_Maybe, bd)) → new_ltEs0(vwx301, vwx401, bd)
new_ltEs(@2(vwx300, vwx301), @2(vwx400, vwx401), app(app(ty_@2, cc), cd), ce) → new_compare2(vwx300, vwx400, new_esEs4(vwx300, vwx400, cc, cd), cc, cd)
new_ltEs(@2(vwx300, vwx301), @2(vwx400, vwx401), ba, app(app(ty_Either, be), bf)) → new_ltEs1(vwx301, vwx401, be, bf)
new_primCompAux(vwx300, vwx400, vwx49, app(app(ty_@2, he), hf)) → new_compare1(vwx300, vwx400, he, hf)
new_compare4(vwx300, vwx400, cg, da) → new_compare21(vwx300, vwx400, new_esEs6(vwx300, vwx400, cg, da), cg, da)
new_compare20(vwx300, vwx400, False, cf) → new_ltEs0(vwx300, vwx400, cf)
new_ltEs1(Left(vwx300), Left(vwx400), app(app(app(ty_@3, fg), fh), ga), fa) → new_ltEs3(vwx300, vwx400, fg, fh, ga)
new_primCompAux(vwx300, vwx400, vwx49, app(ty_Maybe, hg)) → new_compare3(vwx300, vwx400, hg)
new_lt0(vwx300, vwx400, cf) → new_compare20(vwx300, vwx400, new_esEs5(vwx300, vwx400, cf), cf)
new_compare1(vwx300, vwx400, cc, cd) → new_compare2(vwx300, vwx400, new_esEs4(vwx300, vwx400, cc, cd), cc, cd)
new_ltEs(@2(vwx300, vwx301), @2(vwx400, vwx401), app(app(app(ty_@3, dc), dd), de), ce) → new_compare22(vwx300, vwx400, new_esEs7(vwx300, vwx400, dc, dd, de), dc, dd, de)
new_ltEs3(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), app(ty_Maybe, bde), bag, bcc) → new_lt0(vwx300, vwx400, bde)
The TRS R consists of the following rules:
new_ltEs5(Left(vwx300), Left(vwx400), ty_Double, fa) → new_ltEs15(vwx300, vwx400)
new_ltEs19(vwx302, vwx402, ty_Ordering) → new_ltEs16(vwx302, vwx402)
new_lt19(vwx301, vwx401, app(app(ty_Either, bce), bcf)) → new_lt14(vwx301, vwx401, bce, bcf)
new_ltEs16(GT, GT) → True
new_ltEs11(Just(vwx300), Just(vwx400), ty_Integer) → new_ltEs14(vwx300, vwx400)
new_ltEs10(False, True) → True
new_lt19(vwx301, vwx401, app(ty_[], bcg)) → new_lt17(vwx301, vwx401, bcg)
new_ltEs5(Right(vwx300), Right(vwx400), gb, ty_Float) → new_ltEs12(vwx300, vwx400)
new_lt14(vwx300, vwx400, cg, da) → new_esEs20(new_compare31(vwx300, vwx400, cg, da))
new_esEs9(vwx370, vwx380, app(ty_[], bgd)) → new_esEs10(vwx370, vwx380, bgd)
new_esEs23(vwx370, vwx380, app(app(ty_@2, cch), cda)) → new_esEs4(vwx370, vwx380, cch, cda)
new_ltEs5(Left(vwx300), Left(vwx400), ty_Bool, fa) → new_ltEs10(vwx300, vwx400)
new_esEs8(vwx371, vwx381, ty_Integer) → new_esEs16(vwx371, vwx381)
new_compare33(vwx300, vwx400, app(app(app(ty_@3, bac), bad), bae)) → new_compare14(vwx300, vwx400, bac, bad, bae)
new_esEs6(Right(vwx370), Right(vwx380), cgf, ty_Int) → new_esEs13(vwx370, vwx380)
new_ltEs16(LT, GT) → True
new_lt20(vwx300, vwx400, app(app(ty_Either, bdf), bdg)) → new_lt14(vwx300, vwx400, bdf, bdg)
new_esEs27(vwx37, vwx38, ty_Ordering) → new_esEs19(vwx37, vwx38)
new_lt19(vwx301, vwx401, ty_Double) → new_lt15(vwx301, vwx401)
new_ltEs6(vwx301, vwx401, app(ty_Ratio, bhb)) → new_ltEs9(vwx301, vwx401, bhb)
new_ltEs19(vwx302, vwx402, app(ty_Maybe, bbb)) → new_ltEs11(vwx302, vwx402, bbb)
new_ltEs14(vwx30, vwx40) → new_not(new_compare9(vwx30, vwx40))
new_esEs27(vwx37, vwx38, ty_Bool) → new_esEs17(vwx37, vwx38)
new_lt20(vwx300, vwx400, ty_@0) → new_lt6(vwx300, vwx400)
new_compare26(vwx300, vwx400, False, cf) → new_compare19(vwx300, vwx400, new_ltEs11(vwx300, vwx400, cf), cf)
new_primMulNat0(Zero, Zero) → Zero
new_lt4(vwx300, vwx400, ty_Float) → new_lt11(vwx300, vwx400)
new_ltEs5(Left(vwx300), Left(vwx400), app(ty_Ratio, bhe), fa) → new_ltEs9(vwx300, vwx400, bhe)
new_esEs6(Left(vwx370), Left(vwx380), app(ty_[], cfh), cfe) → new_esEs10(vwx370, vwx380, cfh)
new_compare16(vwx300, vwx400, cf) → new_compare26(vwx300, vwx400, new_esEs5(vwx300, vwx400, cf), cf)
new_compare33(vwx300, vwx400, ty_Int) → new_compare8(vwx300, vwx400)
new_esEs6(Left(vwx370), Left(vwx380), app(app(app(ty_@3, cgc), cgd), cge), cfe) → new_esEs7(vwx370, vwx380, cgc, cgd, cge)
new_compare19(vwx300, vwx400, True, cf) → LT
new_lt17(vwx300, vwx400, db) → new_esEs20(new_compare0(vwx300, vwx400, db))
new_compare29(vwx300, vwx400, True) → EQ
new_sr(Integer(vwx4000), Integer(vwx3010)) → Integer(new_primMulInt(vwx4000, vwx3010))
new_lt13(vwx300, vwx400) → new_esEs20(new_compare9(vwx300, vwx400))
new_esEs9(vwx370, vwx380, ty_@0) → new_esEs15(vwx370, vwx380)
new_esEs20(EQ) → False
new_esEs21(vwx372, vwx382, app(ty_[], caf)) → new_esEs10(vwx372, vwx382, caf)
new_esEs21(vwx372, vwx382, ty_Bool) → new_esEs17(vwx372, vwx382)
new_ltEs19(vwx302, vwx402, ty_Integer) → new_ltEs14(vwx302, vwx402)
new_lt20(vwx300, vwx400, app(app(app(ty_@3, bea), beb), bec)) → new_lt18(vwx300, vwx400, bea, beb, bec)
new_not(GT) → False
new_compare19(vwx300, vwx400, False, cf) → GT
new_esEs6(Right(vwx370), Right(vwx380), cgf, ty_Float) → new_esEs11(vwx370, vwx380)
new_esEs17(True, True) → True
new_lt7(vwx300, vwx400, bhc) → new_esEs20(new_compare7(vwx300, vwx400, bhc))
new_lt8(vwx300, vwx400) → new_esEs20(new_compare18(vwx300, vwx400))
new_compare33(vwx300, vwx400, app(ty_Ratio, dcc)) → new_compare7(vwx300, vwx400, dcc)
new_esEs21(vwx372, vwx382, ty_Double) → new_esEs18(vwx372, vwx382)
new_ltEs5(Right(vwx300), Right(vwx400), gb, ty_Integer) → new_ltEs14(vwx300, vwx400)
new_ltEs5(Left(vwx300), Right(vwx400), gb, fa) → True
new_ltEs6(vwx301, vwx401, app(app(app(ty_@3, bh), ca), cb)) → new_ltEs18(vwx301, vwx401, bh, ca, cb)
new_esEs21(vwx372, vwx382, app(app(app(ty_@3, cba), cbb), cbc)) → new_esEs7(vwx372, vwx382, cba, cbb, cbc)
new_lt20(vwx300, vwx400, app(app(ty_@2, bdc), bdd)) → new_lt9(vwx300, vwx400, bdc, bdd)
new_ltEs5(Right(vwx300), Right(vwx400), gb, app(app(ty_@2, gc), gd)) → new_ltEs4(vwx300, vwx400, gc, gd)
new_esEs5(Just(vwx370), Just(vwx380), app(ty_Maybe, ceg)) → new_esEs5(vwx370, vwx380, ceg)
new_ltEs11(Just(vwx300), Just(vwx400), ty_Ordering) → new_ltEs16(vwx300, vwx400)
new_compare27(vwx300, vwx400, False) → new_compare10(vwx300, vwx400, new_ltEs10(vwx300, vwx400))
new_ltEs5(Right(vwx300), Right(vwx400), gb, app(app(ty_Either, gf), gg)) → new_ltEs5(vwx300, vwx400, gf, gg)
new_esEs21(vwx372, vwx382, app(app(ty_Either, cab), cac)) → new_esEs6(vwx372, vwx382, cab, cac)
new_esEs6(Left(vwx370), Left(vwx380), ty_Bool, cfe) → new_esEs17(vwx370, vwx380)
new_esEs8(vwx371, vwx381, app(app(ty_Either, bef), beg)) → new_esEs6(vwx371, vwx381, bef, beg)
new_ltEs10(False, False) → True
new_esEs8(vwx371, vwx381, app(app(ty_@2, beh), bfa)) → new_esEs4(vwx371, vwx381, beh, bfa)
new_ltEs5(Right(vwx300), Left(vwx400), gb, fa) → False
new_esEs6(Left(vwx370), Left(vwx380), ty_Float, cfe) → new_esEs11(vwx370, vwx380)
new_esEs6(Left(vwx370), Left(vwx380), ty_@0, cfe) → new_esEs15(vwx370, vwx380)
new_esEs19(GT, GT) → True
new_ltEs11(Just(vwx300), Just(vwx400), app(ty_[], ec)) → new_ltEs17(vwx300, vwx400, ec)
new_esEs27(vwx37, vwx38, ty_Float) → new_esEs11(vwx37, vwx38)
new_esEs6(Left(vwx370), Left(vwx380), app(app(ty_@2, cff), cfg), cfe) → new_esEs4(vwx370, vwx380, cff, cfg)
new_compare18(vwx300, vwx400) → new_compare27(vwx300, vwx400, new_esEs17(vwx300, vwx400))
new_lt19(vwx301, vwx401, app(ty_Ratio, dbh)) → new_lt7(vwx301, vwx401, dbh)
new_ltEs19(vwx302, vwx402, app(app(ty_@2, bah), bba)) → new_ltEs4(vwx302, vwx402, bah, bba)
new_lt11(vwx300, vwx400) → new_esEs20(new_compare17(vwx300, vwx400))
new_esEs8(vwx371, vwx381, ty_Char) → new_esEs14(vwx371, vwx381)
new_esEs22(vwx371, vwx381, ty_@0) → new_esEs15(vwx371, vwx381)
new_lt4(vwx300, vwx400, ty_Ordering) → new_lt16(vwx300, vwx400)
new_esEs22(vwx371, vwx381, app(app(ty_@2, cbf), cbg)) → new_esEs4(vwx371, vwx381, cbf, cbg)
new_ltEs16(EQ, GT) → True
new_ltEs5(Left(vwx300), Left(vwx400), ty_Float, fa) → new_ltEs12(vwx300, vwx400)
new_ltEs5(Right(vwx300), Right(vwx400), gb, ty_Ordering) → new_ltEs16(vwx300, vwx400)
new_compare11(vwx300, vwx400, False, dc, dd, de) → GT
new_esEs7(@3(vwx370, vwx371, vwx372), @3(vwx380, vwx381, vwx382), bhg, bhh, caa) → new_asAs(new_esEs23(vwx370, vwx380, bhg), new_asAs(new_esEs22(vwx371, vwx381, bhh), new_esEs21(vwx372, vwx382, caa)))
new_compare15(@0, @0) → EQ
new_esEs5(Just(vwx370), Just(vwx380), ty_Ordering) → new_esEs19(vwx370, vwx380)
new_compare33(vwx300, vwx400, ty_@0) → new_compare15(vwx300, vwx400)
new_lt19(vwx301, vwx401, app(ty_Maybe, bcd)) → new_lt10(vwx301, vwx401, bcd)
new_compare13(vwx300, vwx400, False, cg, da) → GT
new_lt4(vwx300, vwx400, app(ty_Ratio, bhc)) → new_lt7(vwx300, vwx400, bhc)
new_esEs9(vwx370, vwx380, ty_Double) → new_esEs18(vwx370, vwx380)
new_ltEs19(vwx302, vwx402, ty_Int) → new_ltEs7(vwx302, vwx402)
new_lt19(vwx301, vwx401, ty_Int) → new_lt5(vwx301, vwx401)
new_esEs23(vwx370, vwx380, app(app(app(ty_@3, cde), cdf), cdg)) → new_esEs7(vwx370, vwx380, cde, cdf, cdg)
new_primCmpNat0(Zero, Succ(vwx4000)) → LT
new_ltEs5(Left(vwx300), Left(vwx400), ty_Int, fa) → new_ltEs7(vwx300, vwx400)
new_esEs27(vwx37, vwx38, app(app(app(ty_@3, bhg), bhh), caa)) → new_esEs7(vwx37, vwx38, bhg, bhh, caa)
new_lt4(vwx300, vwx400, app(app(app(ty_@3, dc), dd), de)) → new_lt18(vwx300, vwx400, dc, dd, de)
new_esEs6(Right(vwx370), Left(vwx380), cgf, cfe) → False
new_esEs6(Left(vwx370), Right(vwx380), cgf, cfe) → False
new_esEs6(Right(vwx370), Right(vwx380), cgf, app(ty_[], chc)) → new_esEs10(vwx370, vwx380, chc)
new_compare25(vwx300, vwx400, True, dc, dd, de) → EQ
new_lt20(vwx300, vwx400, ty_Int) → new_lt5(vwx300, vwx400)
new_esEs8(vwx371, vwx381, app(ty_Ratio, bfc)) → new_esEs12(vwx371, vwx381, bfc)
new_ltEs6(vwx301, vwx401, ty_Char) → new_ltEs13(vwx301, vwx401)
new_compare0([], [], hd) → EQ
new_primEqNat0(Zero, Zero) → True
new_lt18(vwx300, vwx400, dc, dd, de) → new_esEs20(new_compare14(vwx300, vwx400, dc, dd, de))
new_ltEs11(Nothing, Just(vwx400), dbd) → True
new_esEs6(Right(vwx370), Right(vwx380), cgf, ty_Integer) → new_esEs16(vwx370, vwx380)
new_ltEs6(vwx301, vwx401, ty_Ordering) → new_ltEs16(vwx301, vwx401)
new_ltEs5(Right(vwx300), Right(vwx400), gb, app(app(app(ty_@3, ha), hb), hc)) → new_ltEs18(vwx300, vwx400, ha, hb, hc)
new_ltEs11(Just(vwx300), Just(vwx400), app(ty_Maybe, dh)) → new_ltEs11(vwx300, vwx400, dh)
new_esEs6(Right(vwx370), Right(vwx380), cgf, ty_@0) → new_esEs15(vwx370, vwx380)
new_esEs23(vwx370, vwx380, app(app(ty_Either, ccf), ccg)) → new_esEs6(vwx370, vwx380, ccf, ccg)
new_esEs5(Just(vwx370), Just(vwx380), app(app(ty_@2, cec), ced)) → new_esEs4(vwx370, vwx380, cec, ced)
new_esEs23(vwx370, vwx380, ty_Char) → new_esEs14(vwx370, vwx380)
new_esEs6(Right(vwx370), Right(vwx380), cgf, app(app(ty_Either, cgg), cgh)) → new_esEs6(vwx370, vwx380, cgg, cgh)
new_ltEs5(Left(vwx300), Left(vwx400), app(ty_[], ff), fa) → new_ltEs17(vwx300, vwx400, ff)
new_esEs17(False, False) → True
new_esEs17(True, False) → False
new_esEs17(False, True) → False
new_ltEs16(EQ, LT) → False
new_ltEs11(Just(vwx300), Just(vwx400), ty_@0) → new_ltEs8(vwx300, vwx400)
new_esEs6(Right(vwx370), Right(vwx380), cgf, ty_Bool) → new_esEs17(vwx370, vwx380)
new_ltEs11(Just(vwx300), Just(vwx400), app(app(app(ty_@3, ed), ee), ef)) → new_ltEs18(vwx300, vwx400, ed, ee, ef)
new_ltEs16(GT, EQ) → False
new_esEs25(vwx371, vwx381, ty_Int) → new_esEs13(vwx371, vwx381)
new_esEs24(vwx370, vwx380, ty_Bool) → new_esEs17(vwx370, vwx380)
new_compare12(vwx300, vwx400, False, cc, cd) → GT
new_esEs9(vwx370, vwx380, app(app(app(ty_@3, bgg), bgh), bha)) → new_esEs7(vwx370, vwx380, bgg, bgh, bha)
new_esEs22(vwx371, vwx381, app(ty_Ratio, cca)) → new_esEs12(vwx371, vwx381, cca)
new_lt12(vwx300, vwx400) → new_esEs20(new_compare6(vwx300, vwx400))
new_primPlusNat0(Succ(vwx670), vwx30100) → Succ(Succ(new_primPlusNat1(vwx670, vwx30100)))
new_esEs13(vwx37, vwx38) → new_primEqInt(vwx37, vwx38)
new_compare14(vwx300, vwx400, dc, dd, de) → new_compare25(vwx300, vwx400, new_esEs7(vwx300, vwx400, dc, dd, de), dc, dd, de)
new_ltEs11(Just(vwx300), Just(vwx400), ty_Float) → new_ltEs12(vwx300, vwx400)
new_esEs21(vwx372, vwx382, ty_Ordering) → new_esEs19(vwx372, vwx382)
new_esEs9(vwx370, vwx380, ty_Char) → new_esEs14(vwx370, vwx380)
new_esEs8(vwx371, vwx381, ty_Bool) → new_esEs17(vwx371, vwx381)
new_compare17(Float(vwx300, vwx301), Float(vwx400, vwx401)) → new_compare8(new_sr0(vwx300, vwx400), new_sr0(vwx301, vwx401))
new_ltEs5(Left(vwx300), Left(vwx400), app(app(ty_@2, eg), eh), fa) → new_ltEs4(vwx300, vwx400, eg, eh)
new_esEs22(vwx371, vwx381, ty_Char) → new_esEs14(vwx371, vwx381)
new_ltEs15(vwx30, vwx40) → new_not(new_compare32(vwx30, vwx40))
new_ltEs12(vwx30, vwx40) → new_not(new_compare17(vwx30, vwx40))
new_lt19(vwx301, vwx401, ty_Bool) → new_lt8(vwx301, vwx401)
new_primEqInt(Neg(Succ(vwx3700)), Neg(Succ(vwx3800))) → new_primEqNat0(vwx3700, vwx3800)
new_lt5(vwx300, vwx400) → new_esEs20(new_compare8(vwx300, vwx400))
new_ltEs16(LT, EQ) → True
new_compare13(vwx300, vwx400, True, cg, da) → LT
new_esEs6(Right(vwx370), Right(vwx380), cgf, app(app(app(ty_@3, chf), chg), chh)) → new_esEs7(vwx370, vwx380, chf, chg, chh)
new_esEs9(vwx370, vwx380, ty_Integer) → new_esEs16(vwx370, vwx380)
new_esEs19(EQ, EQ) → True
new_ltEs6(vwx301, vwx401, ty_Float) → new_ltEs12(vwx301, vwx401)
new_esEs22(vwx371, vwx381, ty_Ordering) → new_esEs19(vwx371, vwx381)
new_primPlusNat1(Succ(vwx6700), Zero) → Succ(vwx6700)
new_primPlusNat1(Zero, Succ(vwx301000)) → Succ(vwx301000)
new_esEs5(Just(vwx370), Just(vwx380), ty_@0) → new_esEs15(vwx370, vwx380)
new_ltEs5(Left(vwx300), Left(vwx400), ty_Integer, fa) → new_ltEs14(vwx300, vwx400)
new_esEs8(vwx371, vwx381, ty_@0) → new_esEs15(vwx371, vwx381)
new_ltEs5(Left(vwx300), Left(vwx400), ty_@0, fa) → new_ltEs8(vwx300, vwx400)
new_esEs21(vwx372, vwx382, ty_@0) → new_esEs15(vwx372, vwx382)
new_lt4(vwx300, vwx400, app(ty_[], db)) → new_lt17(vwx300, vwx400, db)
new_ltEs19(vwx302, vwx402, app(ty_Ratio, dbg)) → new_ltEs9(vwx302, vwx402, dbg)
new_ltEs8(vwx30, vwx40) → new_not(new_compare15(vwx30, vwx40))
new_lt4(vwx300, vwx400, ty_Char) → new_lt12(vwx300, vwx400)
new_ltEs5(Left(vwx300), Left(vwx400), ty_Char, fa) → new_ltEs13(vwx300, vwx400)
new_esEs9(vwx370, vwx380, ty_Float) → new_esEs11(vwx370, vwx380)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_compare11(vwx300, vwx400, True, dc, dd, de) → LT
new_esEs8(vwx371, vwx381, ty_Double) → new_esEs18(vwx371, vwx381)
new_compare8(vwx30, vwx40) → new_primCmpInt(vwx30, vwx40)
new_lt19(vwx301, vwx401, ty_Char) → new_lt12(vwx301, vwx401)
new_primEqInt(Neg(Succ(vwx3700)), Neg(Zero)) → False
new_primEqInt(Neg(Zero), Neg(Succ(vwx3800))) → False
new_primCompAux0(vwx53, GT) → GT
new_esEs23(vwx370, vwx380, ty_Integer) → new_esEs16(vwx370, vwx380)
new_esEs4(@2(vwx370, vwx371), @2(vwx380, vwx381), bed, bee) → new_asAs(new_esEs9(vwx370, vwx380, bed), new_esEs8(vwx371, vwx381, bee))
new_compare24(vwx300, vwx400, True, cg, da) → EQ
new_lt4(vwx300, vwx400, ty_Bool) → new_lt8(vwx300, vwx400)
new_esEs23(vwx370, vwx380, ty_Ordering) → new_esEs19(vwx370, vwx380)
new_compare32(Double(vwx300, vwx301), Double(vwx400, vwx401)) → new_compare8(new_sr0(vwx300, vwx400), new_sr0(vwx301, vwx401))
new_ltEs6(vwx301, vwx401, ty_@0) → new_ltEs8(vwx301, vwx401)
new_lt19(vwx301, vwx401, ty_Float) → new_lt11(vwx301, vwx401)
new_primCmpInt(Neg(Zero), Pos(Zero)) → EQ
new_primCmpInt(Pos(Zero), Neg(Zero)) → EQ
new_lt19(vwx301, vwx401, ty_Ordering) → new_lt16(vwx301, vwx401)
new_esEs10([], :(vwx380, vwx381), daa) → False
new_esEs10(:(vwx370, vwx371), [], daa) → False
new_ltEs16(GT, LT) → False
new_lt20(vwx300, vwx400, ty_Integer) → new_lt13(vwx300, vwx400)
new_primCmpNat0(Succ(vwx3000), Succ(vwx4000)) → new_primCmpNat0(vwx3000, vwx4000)
new_esEs19(LT, EQ) → False
new_esEs19(EQ, LT) → False
new_esEs26(vwx370, vwx380, ty_Integer) → new_esEs16(vwx370, vwx380)
new_ltEs17(vwx30, vwx40, hd) → new_not(new_compare0(vwx30, vwx40, hd))
new_primEqInt(Pos(Succ(vwx3700)), Pos(Succ(vwx3800))) → new_primEqNat0(vwx3700, vwx3800)
new_compare33(vwx300, vwx400, app(ty_[], bab)) → new_compare0(vwx300, vwx400, bab)
new_ltEs6(vwx301, vwx401, app(app(ty_@2, bb), bc)) → new_ltEs4(vwx301, vwx401, bb, bc)
new_lt15(vwx300, vwx400) → new_esEs20(new_compare32(vwx300, vwx400))
new_ltEs5(Left(vwx300), Left(vwx400), app(app(ty_Either, fc), fd), fa) → new_ltEs5(vwx300, vwx400, fc, fd)
new_compare12(vwx300, vwx400, True, cc, cd) → LT
new_esEs8(vwx371, vwx381, app(ty_Maybe, bfd)) → new_esEs5(vwx371, vwx381, bfd)
new_ltEs5(Right(vwx300), Right(vwx400), gb, app(ty_Maybe, ge)) → new_ltEs11(vwx300, vwx400, ge)
new_compare33(vwx300, vwx400, app(ty_Maybe, hg)) → new_compare16(vwx300, vwx400, hg)
new_esEs10([], [], daa) → True
new_esEs26(vwx370, vwx380, ty_Int) → new_esEs13(vwx370, vwx380)
new_primEqNat0(Succ(vwx3700), Succ(vwx3800)) → new_primEqNat0(vwx3700, vwx3800)
new_primCompAux1(vwx300, vwx400, vwx49, hd) → new_primCompAux0(vwx49, new_compare33(vwx300, vwx400, hd))
new_esEs21(vwx372, vwx382, app(ty_Ratio, cag)) → new_esEs12(vwx372, vwx382, cag)
new_lt6(vwx300, vwx400) → new_esEs20(new_compare15(vwx300, vwx400))
new_esEs22(vwx371, vwx381, ty_Int) → new_esEs13(vwx371, vwx381)
new_esEs24(vwx370, vwx380, app(ty_Ratio, dag)) → new_esEs12(vwx370, vwx380, dag)
new_esEs9(vwx370, vwx380, app(app(ty_Either, bfh), bga)) → new_esEs6(vwx370, vwx380, bfh, bga)
new_ltEs19(vwx302, vwx402, app(app(app(ty_@3, bbf), bbg), bbh)) → new_ltEs18(vwx302, vwx402, bbf, bbg, bbh)
new_ltEs19(vwx302, vwx402, app(ty_[], bbe)) → new_ltEs17(vwx302, vwx402, bbe)
new_primCmpInt(Neg(Succ(vwx3000)), Neg(vwx400)) → new_primCmpNat0(vwx400, Succ(vwx3000))
new_compare7(:%(vwx300, vwx301), :%(vwx400, vwx401), ty_Int) → new_compare8(new_sr0(vwx300, vwx401), new_sr0(vwx400, vwx301))
new_compare33(vwx300, vwx400, ty_Char) → new_compare6(vwx300, vwx400)
new_lt19(vwx301, vwx401, app(app(ty_@2, bca), bcb)) → new_lt9(vwx301, vwx401, bca, bcb)
new_esEs6(Right(vwx370), Right(vwx380), cgf, app(ty_Maybe, che)) → new_esEs5(vwx370, vwx380, che)
new_ltEs6(vwx301, vwx401, app(ty_[], bg)) → new_ltEs17(vwx301, vwx401, bg)
new_compare33(vwx300, vwx400, app(app(ty_Either, hh), baa)) → new_compare31(vwx300, vwx400, hh, baa)
new_esEs8(vwx371, vwx381, app(ty_[], bfb)) → new_esEs10(vwx371, vwx381, bfb)
new_primEqInt(Pos(Succ(vwx3700)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Pos(Succ(vwx3800))) → False
new_lt4(vwx300, vwx400, app(app(ty_@2, cc), cd)) → new_lt9(vwx300, vwx400, cc, cd)
new_primCmpNat0(Zero, Zero) → EQ
new_primCmpNat0(Succ(vwx3000), Zero) → GT
new_ltEs6(vwx301, vwx401, ty_Double) → new_ltEs15(vwx301, vwx401)
new_compare33(vwx300, vwx400, app(app(ty_@2, he), hf)) → new_compare30(vwx300, vwx400, he, hf)
new_esEs24(vwx370, vwx380, ty_@0) → new_esEs15(vwx370, vwx380)
new_primCmpInt(Neg(Zero), Pos(Succ(vwx4000))) → LT
new_esEs24(vwx370, vwx380, ty_Double) → new_esEs18(vwx370, vwx380)
new_primPlusNat1(Succ(vwx6700), Succ(vwx301000)) → Succ(Succ(new_primPlusNat1(vwx6700, vwx301000)))
new_ltEs5(Left(vwx300), Left(vwx400), app(app(app(ty_@3, fg), fh), ga), fa) → new_ltEs18(vwx300, vwx400, fg, fh, ga)
new_ltEs6(vwx301, vwx401, app(ty_Maybe, bd)) → new_ltEs11(vwx301, vwx401, bd)
new_primEqInt(Pos(Succ(vwx3700)), Neg(vwx380)) → False
new_primEqInt(Neg(Succ(vwx3700)), Pos(vwx380)) → False
new_esEs24(vwx370, vwx380, app(app(ty_@2, dad), dae)) → new_esEs4(vwx370, vwx380, dad, dae)
new_esEs27(vwx37, vwx38, app(ty_Maybe, cdh)) → new_esEs5(vwx37, vwx38, cdh)
new_esEs6(Right(vwx370), Right(vwx380), cgf, ty_Ordering) → new_esEs19(vwx370, vwx380)
new_esEs23(vwx370, vwx380, app(ty_Ratio, cdc)) → new_esEs12(vwx370, vwx380, cdc)
new_lt4(vwx300, vwx400, ty_Double) → new_lt15(vwx300, vwx400)
new_primEqInt(Pos(Zero), Neg(Succ(vwx3800))) → False
new_primEqInt(Neg(Zero), Pos(Succ(vwx3800))) → False
new_primCmpInt(Pos(Zero), Pos(Succ(vwx4000))) → new_primCmpNat0(Zero, Succ(vwx4000))
new_esEs27(vwx37, vwx38, ty_Int) → new_esEs13(vwx37, vwx38)
new_compare33(vwx300, vwx400, ty_Integer) → new_compare9(vwx300, vwx400)
new_pePe(False, vwx37, vwx38, vwx39, dcb) → new_asAs(new_esEs27(vwx37, vwx38, dcb), vwx39)
new_esEs6(Right(vwx370), Right(vwx380), cgf, ty_Double) → new_esEs18(vwx370, vwx380)
new_ltEs16(EQ, EQ) → True
new_compare24(vwx300, vwx400, False, cg, da) → new_compare13(vwx300, vwx400, new_ltEs5(vwx300, vwx400, cg, da), cg, da)
new_compare28(vwx300, vwx400) → new_compare29(vwx300, vwx400, new_esEs19(vwx300, vwx400))
new_compare26(vwx300, vwx400, True, cf) → EQ
new_primCompAux0(vwx53, LT) → LT
new_esEs6(Left(vwx370), Left(vwx380), ty_Char, cfe) → new_esEs14(vwx370, vwx380)
new_esEs23(vwx370, vwx380, ty_Float) → new_esEs11(vwx370, vwx380)
new_esEs6(Left(vwx370), Left(vwx380), app(app(ty_Either, cfc), cfd), cfe) → new_esEs6(vwx370, vwx380, cfc, cfd)
new_esEs6(Left(vwx370), Left(vwx380), app(ty_Ratio, cga), cfe) → new_esEs12(vwx370, vwx380, cga)
new_lt20(vwx300, vwx400, ty_Bool) → new_lt8(vwx300, vwx400)
new_esEs24(vwx370, vwx380, ty_Int) → new_esEs13(vwx370, vwx380)
new_primCmpInt(Pos(Succ(vwx3000)), Pos(vwx400)) → new_primCmpNat0(Succ(vwx3000), vwx400)
new_ltEs5(Left(vwx300), Left(vwx400), ty_Ordering, fa) → new_ltEs16(vwx300, vwx400)
new_primPlusNat0(Zero, vwx30100) → Succ(vwx30100)
new_esEs23(vwx370, vwx380, ty_@0) → new_esEs15(vwx370, vwx380)
new_esEs22(vwx371, vwx381, ty_Float) → new_esEs11(vwx371, vwx381)
new_esEs5(Just(vwx370), Just(vwx380), ty_Char) → new_esEs14(vwx370, vwx380)
new_esEs8(vwx371, vwx381, ty_Ordering) → new_esEs19(vwx371, vwx381)
new_esEs24(vwx370, vwx380, app(app(ty_Either, dab), dac)) → new_esEs6(vwx370, vwx380, dab, dac)
new_esEs22(vwx371, vwx381, ty_Bool) → new_esEs17(vwx371, vwx381)
new_compare25(vwx300, vwx400, False, dc, dd, de) → new_compare11(vwx300, vwx400, new_ltEs18(vwx300, vwx400, dc, dd, de), dc, dd, de)
new_lt4(vwx300, vwx400, app(app(ty_Either, cg), da)) → new_lt14(vwx300, vwx400, cg, da)
new_esEs24(vwx370, vwx380, ty_Ordering) → new_esEs19(vwx370, vwx380)
new_esEs9(vwx370, vwx380, app(ty_Maybe, bgf)) → new_esEs5(vwx370, vwx380, bgf)
new_not0 → True
new_compare0(:(vwx300, vwx301), [], hd) → GT
new_esEs23(vwx370, vwx380, app(ty_[], cdb)) → new_esEs10(vwx370, vwx380, cdb)
new_esEs27(vwx37, vwx38, app(app(ty_Either, cgf), cfe)) → new_esEs6(vwx37, vwx38, cgf, cfe)
new_esEs24(vwx370, vwx380, app(ty_Maybe, dah)) → new_esEs5(vwx370, vwx380, dah)
new_esEs6(Right(vwx370), Right(vwx380), cgf, ty_Char) → new_esEs14(vwx370, vwx380)
new_esEs19(LT, GT) → False
new_esEs19(GT, LT) → False
new_esEs6(Right(vwx370), Right(vwx380), cgf, app(ty_Ratio, chd)) → new_esEs12(vwx370, vwx380, chd)
new_esEs5(Just(vwx370), Just(vwx380), ty_Float) → new_esEs11(vwx370, vwx380)
new_primCmpInt(Pos(Succ(vwx3000)), Neg(vwx400)) → GT
new_esEs8(vwx371, vwx381, app(app(app(ty_@3, bfe), bff), bfg)) → new_esEs7(vwx371, vwx381, bfe, bff, bfg)
new_esEs22(vwx371, vwx381, app(app(app(ty_@3, ccc), ccd), cce)) → new_esEs7(vwx371, vwx381, ccc, ccd, cce)
new_esEs6(Left(vwx370), Left(vwx380), ty_Double, cfe) → new_esEs18(vwx370, vwx380)
new_esEs21(vwx372, vwx382, ty_Integer) → new_esEs16(vwx372, vwx382)
new_lt4(vwx300, vwx400, ty_@0) → new_lt6(vwx300, vwx400)
new_ltEs11(Just(vwx300), Just(vwx400), ty_Double) → new_ltEs15(vwx300, vwx400)
new_esEs27(vwx37, vwx38, ty_@0) → new_esEs15(vwx37, vwx38)
new_lt20(vwx300, vwx400, ty_Double) → new_lt15(vwx300, vwx400)
new_primMulInt(Pos(vwx4000), Pos(vwx3010)) → Pos(new_primMulNat0(vwx4000, vwx3010))
new_esEs22(vwx371, vwx381, ty_Double) → new_esEs18(vwx371, vwx381)
new_esEs5(Just(vwx370), Just(vwx380), ty_Bool) → new_esEs17(vwx370, vwx380)
new_esEs21(vwx372, vwx382, app(app(ty_@2, cad), cae)) → new_esEs4(vwx372, vwx382, cad, cae)
new_esEs24(vwx370, vwx380, ty_Integer) → new_esEs16(vwx370, vwx380)
new_esEs5(Just(vwx370), Just(vwx380), ty_Int) → new_esEs13(vwx370, vwx380)
new_ltEs11(Just(vwx300), Just(vwx400), app(ty_Ratio, dbe)) → new_ltEs9(vwx300, vwx400, dbe)
new_primMulInt(Neg(vwx4000), Neg(vwx3010)) → Pos(new_primMulNat0(vwx4000, vwx3010))
new_esEs5(Just(vwx370), Just(vwx380), ty_Double) → new_esEs18(vwx370, vwx380)
new_ltEs9(vwx30, vwx40, bhd) → new_not(new_compare7(vwx30, vwx40, bhd))
new_compare110(vwx300, vwx400, True) → LT
new_ltEs19(vwx302, vwx402, app(app(ty_Either, bbc), bbd)) → new_ltEs5(vwx302, vwx402, bbc, bbd)
new_compare33(vwx300, vwx400, ty_Ordering) → new_compare28(vwx300, vwx400)
new_primEqNat0(Zero, Succ(vwx3800)) → False
new_primEqNat0(Succ(vwx3700), Zero) → False
new_esEs27(vwx37, vwx38, ty_Char) → new_esEs14(vwx37, vwx38)
new_ltEs18(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), baf, bag, bcc) → new_pePe(new_lt20(vwx300, vwx400, baf), vwx300, vwx400, new_pePe(new_lt19(vwx301, vwx401, bag), vwx301, vwx401, new_ltEs19(vwx302, vwx402, bcc), bag), baf)
new_compare33(vwx300, vwx400, ty_Float) → new_compare17(vwx300, vwx400)
new_lt20(vwx300, vwx400, app(ty_Maybe, bde)) → new_lt10(vwx300, vwx400, bde)
new_compare110(vwx300, vwx400, False) → GT
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs9(vwx370, vwx380, ty_Int) → new_esEs13(vwx370, vwx380)
new_esEs5(Just(vwx370), Just(vwx380), app(ty_[], cee)) → new_esEs10(vwx370, vwx380, cee)
new_ltEs6(vwx301, vwx401, ty_Int) → new_ltEs7(vwx301, vwx401)
new_ltEs19(vwx302, vwx402, ty_Char) → new_ltEs13(vwx302, vwx402)
new_esEs27(vwx37, vwx38, ty_Integer) → new_esEs16(vwx37, vwx38)
new_esEs9(vwx370, vwx380, ty_Ordering) → new_esEs19(vwx370, vwx380)
new_ltEs19(vwx302, vwx402, ty_Bool) → new_ltEs10(vwx302, vwx402)
new_pePe(True, vwx37, vwx38, vwx39, dcb) → True
new_esEs23(vwx370, vwx380, ty_Double) → new_esEs18(vwx370, vwx380)
new_esEs25(vwx371, vwx381, ty_Integer) → new_esEs16(vwx371, vwx381)
new_primCmpInt(Neg(Zero), Neg(Succ(vwx4000))) → new_primCmpNat0(Succ(vwx4000), Zero)
new_compare23(vwx300, vwx400, True, cc, cd) → EQ
new_primCmpInt(Pos(Zero), Neg(Succ(vwx4000))) → GT
new_lt4(vwx300, vwx400, ty_Int) → new_lt5(vwx300, vwx400)
new_esEs23(vwx370, vwx380, ty_Bool) → new_esEs17(vwx370, vwx380)
new_ltEs11(Just(vwx300), Just(vwx400), ty_Bool) → new_ltEs10(vwx300, vwx400)
new_compare0(:(vwx300, vwx301), :(vwx400, vwx401), hd) → new_primCompAux1(vwx300, vwx400, new_compare0(vwx301, vwx401, hd), hd)
new_esEs6(Right(vwx370), Right(vwx380), cgf, app(app(ty_@2, cha), chb)) → new_esEs4(vwx370, vwx380, cha, chb)
new_sr0(vwx400, vwx301) → new_primMulInt(vwx400, vwx301)
new_esEs11(Float(vwx370, vwx371), Float(vwx380, vwx381)) → new_esEs13(new_sr0(vwx370, vwx380), new_sr0(vwx371, vwx381))
new_esEs19(LT, LT) → True
new_compare23(vwx300, vwx400, False, cc, cd) → new_compare12(vwx300, vwx400, new_ltEs4(vwx300, vwx400, cc, cd), cc, cd)
new_esEs27(vwx37, vwx38, app(ty_Ratio, dbf)) → new_esEs12(vwx37, vwx38, dbf)
new_esEs20(GT) → False
new_esEs9(vwx370, vwx380, ty_Bool) → new_esEs17(vwx370, vwx380)
new_esEs23(vwx370, vwx380, ty_Int) → new_esEs13(vwx370, vwx380)
new_esEs16(Integer(vwx370), Integer(vwx380)) → new_primEqInt(vwx370, vwx380)
new_esEs24(vwx370, vwx380, app(ty_[], daf)) → new_esEs10(vwx370, vwx380, daf)
new_esEs19(EQ, GT) → False
new_esEs19(GT, EQ) → False
new_esEs9(vwx370, vwx380, app(app(ty_@2, bgb), bgc)) → new_esEs4(vwx370, vwx380, bgb, bgc)
new_ltEs11(Just(vwx300), Just(vwx400), app(app(ty_Either, ea), eb)) → new_ltEs5(vwx300, vwx400, ea, eb)
new_esEs10(:(vwx370, vwx371), :(vwx380, vwx381), daa) → new_asAs(new_esEs24(vwx370, vwx380, daa), new_esEs10(vwx371, vwx381, daa))
new_esEs27(vwx37, vwx38, ty_Double) → new_esEs18(vwx37, vwx38)
new_lt16(vwx300, vwx400) → new_esEs20(new_compare28(vwx300, vwx400))
new_esEs6(Left(vwx370), Left(vwx380), ty_Ordering, cfe) → new_esEs19(vwx370, vwx380)
new_esEs24(vwx370, vwx380, app(app(app(ty_@3, dba), dbb), dbc)) → new_esEs7(vwx370, vwx380, dba, dbb, dbc)
new_primCmpInt(Neg(Zero), Neg(Zero)) → EQ
new_ltEs5(Right(vwx300), Right(vwx400), gb, app(ty_Ratio, bhf)) → new_ltEs9(vwx300, vwx400, bhf)
new_esEs15(@0, @0) → True
new_ltEs11(Just(vwx300), Just(vwx400), app(app(ty_@2, df), dg)) → new_ltEs4(vwx300, vwx400, df, dg)
new_compare7(:%(vwx300, vwx301), :%(vwx400, vwx401), ty_Integer) → new_compare9(new_sr(vwx300, vwx401), new_sr(vwx400, vwx301))
new_ltEs10(True, False) → False
new_compare9(Integer(vwx300), Integer(vwx400)) → new_primCmpInt(vwx300, vwx400)
new_asAs(False, vwx48) → False
new_primMulInt(Neg(vwx4000), Pos(vwx3010)) → Neg(new_primMulNat0(vwx4000, vwx3010))
new_primMulInt(Pos(vwx4000), Neg(vwx3010)) → Neg(new_primMulNat0(vwx4000, vwx3010))
new_primMulNat0(Zero, Succ(vwx30100)) → Zero
new_primMulNat0(Succ(vwx40000), Zero) → Zero
new_esEs22(vwx371, vwx381, app(ty_[], cbh)) → new_esEs10(vwx371, vwx381, cbh)
new_lt19(vwx301, vwx401, app(app(app(ty_@3, bch), bda), bdb)) → new_lt18(vwx301, vwx401, bch, bda, bdb)
new_esEs24(vwx370, vwx380, ty_Float) → new_esEs11(vwx370, vwx380)
new_ltEs5(Right(vwx300), Right(vwx400), gb, ty_Int) → new_ltEs7(vwx300, vwx400)
new_not(EQ) → new_not0
new_lt20(vwx300, vwx400, app(ty_[], bdh)) → new_lt17(vwx300, vwx400, bdh)
new_ltEs7(vwx30, vwx40) → new_not(new_compare8(vwx30, vwx40))
new_esEs23(vwx370, vwx380, app(ty_Maybe, cdd)) → new_esEs5(vwx370, vwx380, cdd)
new_ltEs5(Right(vwx300), Right(vwx400), gb, ty_@0) → new_ltEs8(vwx300, vwx400)
new_ltEs11(Just(vwx300), Just(vwx400), ty_Char) → new_ltEs13(vwx300, vwx400)
new_esEs6(Left(vwx370), Left(vwx380), app(ty_Maybe, cgb), cfe) → new_esEs5(vwx370, vwx380, cgb)
new_esEs21(vwx372, vwx382, ty_Int) → new_esEs13(vwx372, vwx382)
new_esEs12(:%(vwx370, vwx371), :%(vwx380, vwx381), dbf) → new_asAs(new_esEs26(vwx370, vwx380, dbf), new_esEs25(vwx371, vwx381, dbf))
new_compare27(vwx300, vwx400, True) → EQ
new_esEs27(vwx37, vwx38, app(ty_[], daa)) → new_esEs10(vwx37, vwx38, daa)
new_esEs20(LT) → True
new_ltEs19(vwx302, vwx402, ty_@0) → new_ltEs8(vwx302, vwx402)
new_esEs5(Nothing, Just(vwx380), cdh) → False
new_esEs5(Just(vwx370), Nothing, cdh) → False
new_esEs14(Char(vwx370), Char(vwx380)) → new_primEqNat0(vwx370, vwx380)
new_lt9(vwx300, vwx400, cc, cd) → new_esEs20(new_compare30(vwx300, vwx400, cc, cd))
new_lt19(vwx301, vwx401, ty_Integer) → new_lt13(vwx301, vwx401)
new_esEs27(vwx37, vwx38, app(app(ty_@2, bed), bee)) → new_esEs4(vwx37, vwx38, bed, bee)
new_ltEs11(Just(vwx300), Just(vwx400), ty_Int) → new_ltEs7(vwx300, vwx400)
new_lt20(vwx300, vwx400, ty_Ordering) → new_lt16(vwx300, vwx400)
new_lt10(vwx300, vwx400, cf) → new_esEs20(new_compare16(vwx300, vwx400, cf))
new_esEs5(Just(vwx370), Just(vwx380), app(app(ty_Either, cea), ceb)) → new_esEs6(vwx370, vwx380, cea, ceb)
new_lt20(vwx300, vwx400, ty_Float) → new_lt11(vwx300, vwx400)
new_ltEs5(Right(vwx300), Right(vwx400), gb, ty_Char) → new_ltEs13(vwx300, vwx400)
new_compare33(vwx300, vwx400, ty_Bool) → new_compare18(vwx300, vwx400)
new_not(LT) → new_not0
new_esEs8(vwx371, vwx381, ty_Int) → new_esEs13(vwx371, vwx381)
new_esEs5(Nothing, Nothing, cdh) → True
new_esEs22(vwx371, vwx381, app(app(ty_Either, cbd), cbe)) → new_esEs6(vwx371, vwx381, cbd, cbe)
new_ltEs5(Right(vwx300), Right(vwx400), gb, ty_Double) → new_ltEs15(vwx300, vwx400)
new_esEs5(Just(vwx370), Just(vwx380), app(app(app(ty_@3, ceh), cfa), cfb)) → new_esEs7(vwx370, vwx380, ceh, cfa, cfb)
new_esEs5(Just(vwx370), Just(vwx380), ty_Integer) → new_esEs16(vwx370, vwx380)
new_esEs6(Left(vwx370), Left(vwx380), ty_Int, cfe) → new_esEs13(vwx370, vwx380)
new_esEs8(vwx371, vwx381, ty_Float) → new_esEs11(vwx371, vwx381)
new_esEs22(vwx371, vwx381, ty_Integer) → new_esEs16(vwx371, vwx381)
new_lt20(vwx300, vwx400, ty_Char) → new_lt12(vwx300, vwx400)
new_ltEs6(vwx301, vwx401, app(app(ty_Either, be), bf)) → new_ltEs5(vwx301, vwx401, be, bf)
new_esEs21(vwx372, vwx382, ty_Float) → new_esEs11(vwx372, vwx382)
new_ltEs19(vwx302, vwx402, ty_Double) → new_ltEs15(vwx302, vwx402)
new_compare31(vwx300, vwx400, cg, da) → new_compare24(vwx300, vwx400, new_esEs6(vwx300, vwx400, cg, da), cg, da)
new_lt19(vwx301, vwx401, ty_@0) → new_lt6(vwx301, vwx401)
new_ltEs5(Right(vwx300), Right(vwx400), gb, app(ty_[], gh)) → new_ltEs17(vwx300, vwx400, gh)
new_esEs22(vwx371, vwx381, app(ty_Maybe, ccb)) → new_esEs5(vwx371, vwx381, ccb)
new_esEs21(vwx372, vwx382, app(ty_Maybe, cah)) → new_esEs5(vwx372, vwx382, cah)
new_esEs6(Left(vwx370), Left(vwx380), ty_Integer, cfe) → new_esEs16(vwx370, vwx380)
new_esEs9(vwx370, vwx380, app(ty_Ratio, bge)) → new_esEs12(vwx370, vwx380, bge)
new_compare0([], :(vwx400, vwx401), hd) → LT
new_primPlusNat1(Zero, Zero) → Zero
new_ltEs10(True, True) → True
new_asAs(True, vwx48) → vwx48
new_primMulNat0(Succ(vwx40000), Succ(vwx30100)) → new_primPlusNat0(new_primMulNat0(vwx40000, Succ(vwx30100)), vwx30100)
new_ltEs11(Nothing, Nothing, dbd) → True
new_ltEs13(vwx30, vwx40) → new_not(new_compare6(vwx30, vwx40))
new_ltEs5(Right(vwx300), Right(vwx400), gb, ty_Bool) → new_ltEs10(vwx300, vwx400)
new_ltEs19(vwx302, vwx402, ty_Float) → new_ltEs12(vwx302, vwx402)
new_ltEs6(vwx301, vwx401, ty_Bool) → new_ltEs10(vwx301, vwx401)
new_esEs5(Just(vwx370), Just(vwx380), app(ty_Ratio, cef)) → new_esEs12(vwx370, vwx380, cef)
new_ltEs16(LT, LT) → True
new_esEs21(vwx372, vwx382, ty_Char) → new_esEs14(vwx372, vwx382)
new_compare30(vwx300, vwx400, cc, cd) → new_compare23(vwx300, vwx400, new_esEs4(vwx300, vwx400, cc, cd), cc, cd)
new_lt4(vwx300, vwx400, ty_Integer) → new_lt13(vwx300, vwx400)
new_esEs24(vwx370, vwx380, ty_Char) → new_esEs14(vwx370, vwx380)
new_lt4(vwx300, vwx400, app(ty_Maybe, cf)) → new_lt10(vwx300, vwx400, cf)
new_compare10(vwx300, vwx400, True) → LT
new_ltEs4(@2(vwx300, vwx301), @2(vwx400, vwx401), ba, ce) → new_pePe(new_lt4(vwx300, vwx400, ba), vwx300, vwx400, new_ltEs6(vwx301, vwx401, ce), ba)
new_lt20(vwx300, vwx400, app(ty_Ratio, dca)) → new_lt7(vwx300, vwx400, dca)
new_ltEs6(vwx301, vwx401, ty_Integer) → new_ltEs14(vwx301, vwx401)
new_compare6(Char(vwx300), Char(vwx400)) → new_primCmpNat0(vwx300, vwx400)
new_compare10(vwx300, vwx400, False) → GT
new_ltEs5(Left(vwx300), Left(vwx400), app(ty_Maybe, fb), fa) → new_ltEs11(vwx300, vwx400, fb)
new_primCmpInt(Pos(Zero), Pos(Zero)) → EQ
new_esEs18(Double(vwx370, vwx371), Double(vwx380, vwx381)) → new_esEs13(new_sr0(vwx370, vwx380), new_sr0(vwx371, vwx381))
new_primCompAux0(vwx53, EQ) → vwx53
new_compare33(vwx300, vwx400, ty_Double) → new_compare32(vwx300, vwx400)
new_ltEs11(Just(vwx300), Nothing, dbd) → False
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primCmpInt(Neg(Succ(vwx3000)), Pos(vwx400)) → LT
new_compare29(vwx300, vwx400, False) → new_compare110(vwx300, vwx400, new_ltEs16(vwx300, vwx400))
The set Q consists of the following terms:
new_esEs24(x0, x1, ty_Ordering)
new_compare33(x0, x1, ty_Bool)
new_esEs10(:(x0, x1), [], x2)
new_compare7(:%(x0, x1), :%(x2, x3), ty_Integer)
new_esEs6(Right(x0), Right(x1), x2, ty_Integer)
new_esEs23(x0, x1, ty_Bool)
new_ltEs19(x0, x1, app(ty_Maybe, x2))
new_compare33(x0, x1, ty_Ordering)
new_primCmpInt(Neg(Succ(x0)), Pos(x1))
new_primCmpInt(Pos(Succ(x0)), Neg(x1))
new_esEs8(x0, x1, app(ty_Ratio, x2))
new_compare19(x0, x1, False, x2)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs9(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_lt19(x0, x1, app(app(ty_@2, x2), x3))
new_ltEs11(Just(x0), Nothing, x1)
new_esEs6(Left(x0), Left(x1), ty_Ordering, x2)
new_compare15(@0, @0)
new_lt17(x0, x1, x2)
new_lt20(x0, x1, app(app(ty_Either, x2), x3))
new_primPlusNat1(Succ(x0), Zero)
new_lt20(x0, x1, ty_Double)
new_ltEs6(x0, x1, ty_Bool)
new_compare17(Float(x0, x1), Float(x2, x3))
new_compare18(x0, x1)
new_esEs9(x0, x1, app(app(ty_@2, x2), x3))
new_ltEs4(@2(x0, x1), @2(x2, x3), x4, x5)
new_ltEs12(x0, x1)
new_lt4(x0, x1, ty_Float)
new_lt20(x0, x1, ty_Integer)
new_ltEs5(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_lt4(x0, x1, ty_Int)
new_esEs21(x0, x1, ty_Int)
new_compare11(x0, x1, True, x2, x3, x4)
new_esEs12(:%(x0, x1), :%(x2, x3), x4)
new_esEs6(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_compare33(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, ty_Char)
new_compare0([], [], x0)
new_ltEs5(Right(x0), Right(x1), x2, ty_Float)
new_esEs5(Just(x0), Just(x1), app(ty_Maybe, x2))
new_primCompAux0(x0, EQ)
new_esEs24(x0, x1, ty_Integer)
new_compare32(Double(x0, x1), Double(x2, x3))
new_esEs6(Right(x0), Right(x1), x2, ty_Char)
new_ltEs5(Left(x0), Left(x1), ty_@0, x2)
new_esEs9(x0, x1, app(ty_[], x2))
new_esEs5(Just(x0), Just(x1), ty_Integer)
new_esEs6(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_compare9(Integer(x0), Integer(x1))
new_compare7(:%(x0, x1), :%(x2, x3), ty_Int)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_ltEs6(x0, x1, ty_Float)
new_lt20(x0, x1, app(ty_Maybe, x2))
new_ltEs19(x0, x1, ty_Char)
new_compare23(x0, x1, True, x2, x3)
new_ltEs5(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_ltEs5(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs27(x0, x1, ty_Double)
new_esEs22(x0, x1, app(ty_[], x2))
new_ltEs5(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs23(x0, x1, ty_Float)
new_ltEs19(x0, x1, app(ty_Ratio, x2))
new_compare28(x0, x1)
new_compare0([], :(x0, x1), x2)
new_ltEs5(Right(x0), Right(x1), x2, ty_Char)
new_lt19(x0, x1, ty_Double)
new_esEs20(LT)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs17(False, False)
new_lt20(x0, x1, ty_Float)
new_compare10(x0, x1, True)
new_esEs5(Nothing, Just(x0), x1)
new_esEs8(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_Float)
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_ltEs5(Right(x0), Right(x1), x2, ty_Int)
new_esEs9(x0, x1, app(app(ty_Either, x2), x3))
new_ltEs5(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_ltEs5(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs8(x0, x1, ty_Int)
new_lt19(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_lt19(x0, x1, app(app(ty_Either, x2), x3))
new_esEs27(x0, x1, ty_Bool)
new_ltEs5(Left(x0), Left(x1), ty_Char, x2)
new_primPlusNat1(Zero, Succ(x0))
new_primEqNat0(Zero, Zero)
new_ltEs5(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs5(Just(x0), Just(x1), ty_@0)
new_compare33(x0, x1, app(app(ty_Either, x2), x3))
new_esEs16(Integer(x0), Integer(x1))
new_esEs9(x0, x1, ty_Float)
new_esEs6(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs9(x0, x1, ty_Integer)
new_esEs10(:(x0, x1), :(x2, x3), x4)
new_ltEs19(x0, x1, ty_Int)
new_ltEs19(x0, x1, ty_Ordering)
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_ltEs5(Left(x0), Left(x1), ty_Integer, x2)
new_esEs22(x0, x1, ty_Double)
new_lt4(x0, x1, ty_@0)
new_esEs6(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs22(x0, x1, ty_Bool)
new_esEs6(Left(x0), Left(x1), ty_Bool, x2)
new_primMulNat0(Zero, Zero)
new_lt20(x0, x1, app(app(ty_@2, x2), x3))
new_ltEs8(x0, x1)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_compare33(x0, x1, app(ty_Ratio, x2))
new_lt10(x0, x1, x2)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_compare33(x0, x1, ty_Int)
new_primMulInt(Pos(x0), Pos(x1))
new_compare33(x0, x1, app(ty_[], x2))
new_lt20(x0, x1, ty_Char)
new_ltEs13(x0, x1)
new_esEs27(x0, x1, ty_Char)
new_esEs6(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs19(LT, LT)
new_esEs21(x0, x1, ty_Float)
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_esEs19(GT, EQ)
new_esEs19(EQ, GT)
new_ltEs11(Just(x0), Just(x1), ty_Bool)
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs9(x0, x1, ty_Bool)
new_primCompAux1(x0, x1, x2, x3)
new_esEs21(x0, x1, ty_@0)
new_primCmpInt(Pos(Zero), Pos(Succ(x0)))
new_esEs10([], :(x0, x1), x2)
new_primMulNat0(Succ(x0), Zero)
new_esEs6(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_lt20(x0, x1, ty_@0)
new_esEs6(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_compare33(x0, x1, ty_@0)
new_esEs6(Left(x0), Left(x1), ty_@0, x2)
new_ltEs5(Right(x0), Right(x1), x2, ty_@0)
new_esEs5(Just(x0), Just(x1), ty_Double)
new_esEs9(x0, x1, ty_Ordering)
new_compare33(x0, x1, ty_Float)
new_esEs6(Right(x0), Right(x1), x2, ty_Float)
new_lt13(x0, x1)
new_ltEs19(x0, x1, app(app(ty_Either, x2), x3))
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_lt9(x0, x1, x2, x3)
new_esEs25(x0, x1, ty_Integer)
new_compare11(x0, x1, False, x2, x3, x4)
new_compare6(Char(x0), Char(x1))
new_esEs7(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_esEs8(x0, x1, app(ty_Maybe, x2))
new_primCompAux0(x0, LT)
new_primCompAux0(x0, GT)
new_primCmpInt(Neg(Zero), Pos(Succ(x0)))
new_primCmpInt(Pos(Zero), Neg(Succ(x0)))
new_ltEs5(Right(x0), Right(x1), x2, ty_Bool)
new_ltEs11(Just(x0), Just(x1), ty_Ordering)
new_ltEs5(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_ltEs19(x0, x1, ty_Bool)
new_esEs23(x0, x1, ty_Integer)
new_esEs9(x0, x1, ty_Double)
new_lt7(x0, x1, x2)
new_esEs24(x0, x1, ty_Char)
new_esEs10([], [], x0)
new_lt19(x0, x1, ty_Ordering)
new_ltEs11(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs21(x0, x1, ty_Double)
new_compare27(x0, x1, False)
new_ltEs11(Just(x0), Just(x1), ty_Float)
new_compare33(x0, x1, app(app(ty_@2, x2), x3))
new_compare29(x0, x1, True)
new_lt12(x0, x1)
new_esEs6(Right(x0), Right(x1), x2, ty_Int)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs27(x0, x1, ty_Float)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primPlusNat1(Zero, Zero)
new_primCmpInt(Neg(Succ(x0)), Neg(x1))
new_ltEs11(Just(x0), Just(x1), ty_Double)
new_not0
new_ltEs16(EQ, EQ)
new_ltEs10(False, False)
new_esEs21(x0, x1, ty_Integer)
new_esEs8(x0, x1, app(app(ty_Either, x2), x3))
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_ltEs11(Just(x0), Just(x1), ty_Char)
new_esEs23(x0, x1, ty_Ordering)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_primCmpInt(Neg(Zero), Neg(Zero))
new_compare33(x0, x1, ty_Integer)
new_ltEs5(Right(x0), Right(x1), x2, app(ty_[], x3))
new_sr0(x0, x1)
new_ltEs16(LT, LT)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs5(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs8(x0, x1, ty_Double)
new_esEs9(x0, x1, ty_Int)
new_ltEs5(Left(x0), Left(x1), app(ty_[], x2), x3)
new_ltEs5(Left(x0), Right(x1), x2, x3)
new_ltEs5(Right(x0), Left(x1), x2, x3)
new_primEqNat0(Succ(x0), Zero)
new_esEs5(Just(x0), Just(x1), ty_Char)
new_esEs5(Just(x0), Just(x1), app(ty_Ratio, x2))
new_ltEs11(Nothing, Just(x0), x1)
new_ltEs5(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs26(x0, x1, ty_Int)
new_esEs6(Left(x0), Left(x1), ty_Integer, x2)
new_esEs5(Just(x0), Just(x1), ty_Int)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_compare25(x0, x1, True, x2, x3, x4)
new_esEs5(Just(x0), Just(x1), ty_Bool)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_ltEs16(GT, LT)
new_ltEs16(LT, GT)
new_ltEs15(x0, x1)
new_compare110(x0, x1, True)
new_esEs24(x0, x1, ty_Float)
new_esEs6(Left(x0), Left(x1), ty_Float, x2)
new_not(GT)
new_esEs24(x0, x1, app(ty_[], x2))
new_lt14(x0, x1, x2, x3)
new_lt4(x0, x1, ty_Char)
new_ltEs19(x0, x1, app(app(ty_@2, x2), x3))
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs21(x0, x1, ty_Char)
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_lt4(x0, x1, app(ty_Maybe, x2))
new_lt11(x0, x1)
new_asAs(True, x0)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs9(x0, x1, ty_Char)
new_ltEs7(x0, x1)
new_esEs8(x0, x1, ty_Bool)
new_esEs27(x0, x1, ty_Int)
new_compare27(x0, x1, True)
new_lt19(x0, x1, ty_Float)
new_esEs5(Just(x0), Just(x1), ty_Float)
new_ltEs6(x0, x1, ty_Int)
new_compare33(x0, x1, ty_Char)
new_primMulNat0(Zero, Succ(x0))
new_esEs23(x0, x1, ty_@0)
new_ltEs6(x0, x1, app(ty_Maybe, x2))
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primCmpInt(Pos(Zero), Pos(Zero))
new_esEs24(x0, x1, ty_Double)
new_esEs23(x0, x1, ty_Char)
new_ltEs6(x0, x1, app(ty_Ratio, x2))
new_lt15(x0, x1)
new_esEs5(Just(x0), Nothing, x1)
new_ltEs5(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs5(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Right(x0), Left(x1), x2, x3)
new_esEs6(Left(x0), Right(x1), x2, x3)
new_lt16(x0, x1)
new_lt4(x0, x1, app(app(ty_@2, x2), x3))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs24(x0, x1, ty_@0)
new_compare26(x0, x1, True, x2)
new_esEs13(x0, x1)
new_esEs6(Right(x0), Right(x1), x2, ty_Bool)
new_lt19(x0, x1, ty_Bool)
new_ltEs19(x0, x1, app(ty_[], x2))
new_ltEs5(Right(x0), Right(x1), x2, ty_Double)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, ty_Bool)
new_ltEs6(x0, x1, app(ty_[], x2))
new_ltEs5(Left(x0), Left(x1), ty_Double, x2)
new_ltEs6(x0, x1, ty_Ordering)
new_lt20(x0, x1, app(ty_[], x2))
new_ltEs16(GT, GT)
new_primCmpNat0(Zero, Succ(x0))
new_compare0(:(x0, x1), :(x2, x3), x4)
new_esEs8(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Int)
new_ltEs19(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare24(x0, x1, False, x2, x3)
new_ltEs11(Just(x0), Just(x1), ty_Int)
new_ltEs19(x0, x1, ty_Integer)
new_lt19(x0, x1, ty_Int)
new_lt18(x0, x1, x2, x3, x4)
new_esEs5(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_compare12(x0, x1, True, x2, x3)
new_esEs21(x0, x1, ty_Ordering)
new_lt4(x0, x1, ty_Bool)
new_lt5(x0, x1)
new_ltEs18(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_lt4(x0, x1, ty_Integer)
new_lt4(x0, x1, ty_Ordering)
new_esEs6(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_compare10(x0, x1, False)
new_esEs26(x0, x1, ty_Integer)
new_esEs21(x0, x1, app(ty_[], x2))
new_ltEs19(x0, x1, ty_Double)
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_lt20(x0, x1, ty_Ordering)
new_ltEs5(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs23(x0, x1, ty_Double)
new_primPlusNat0(Zero, x0)
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_lt4(x0, x1, app(ty_[], x2))
new_primEqNat0(Succ(x0), Succ(x1))
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs27(x0, x1, app(ty_[], x2))
new_pePe(True, x0, x1, x2, x3)
new_compare13(x0, x1, True, x2, x3)
new_lt19(x0, x1, ty_Integer)
new_compare13(x0, x1, False, x2, x3)
new_primCmpNat0(Zero, Zero)
new_esEs8(x0, x1, ty_Ordering)
new_ltEs11(Just(x0), Just(x1), ty_Integer)
new_ltEs11(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_ltEs17(x0, x1, x2)
new_esEs9(x0, x1, app(ty_Ratio, x2))
new_esEs23(x0, x1, ty_Int)
new_ltEs5(Left(x0), Left(x1), ty_Int, x2)
new_ltEs10(True, True)
new_ltEs14(x0, x1)
new_esEs15(@0, @0)
new_esEs27(x0, x1, ty_@0)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_ltEs11(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_pePe(False, x0, x1, x2, x3)
new_esEs8(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare8(x0, x1)
new_esEs19(GT, GT)
new_esEs9(x0, x1, ty_@0)
new_compare0(:(x0, x1), [], x2)
new_lt20(x0, x1, app(ty_Ratio, x2))
new_ltEs6(x0, x1, ty_Integer)
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_ltEs5(Left(x0), Left(x1), ty_Float, x2)
new_esEs24(x0, x1, ty_Int)
new_esEs6(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs19(EQ, EQ)
new_ltEs11(Just(x0), Just(x1), ty_@0)
new_primPlusNat1(Succ(x0), Succ(x1))
new_ltEs19(x0, x1, ty_@0)
new_esEs20(EQ)
new_esEs18(Double(x0, x1), Double(x2, x3))
new_lt19(x0, x1, app(ty_Ratio, x2))
new_lt19(x0, x1, app(ty_Maybe, x2))
new_lt6(x0, x1)
new_primCmpNat0(Succ(x0), Succ(x1))
new_esEs6(Left(x0), Left(x1), ty_Double, x2)
new_compare33(x0, x1, ty_Double)
new_esEs19(EQ, LT)
new_esEs19(LT, EQ)
new_esEs11(Float(x0, x1), Float(x2, x3))
new_esEs25(x0, x1, ty_Int)
new_lt4(x0, x1, app(app(ty_Either, x2), x3))
new_ltEs19(x0, x1, ty_Float)
new_esEs19(GT, LT)
new_esEs19(LT, GT)
new_not(EQ)
new_ltEs5(Left(x0), Left(x1), ty_Bool, x2)
new_ltEs16(GT, EQ)
new_esEs8(x0, x1, app(app(ty_@2, x2), x3))
new_ltEs11(Just(x0), Just(x1), app(ty_[], x2))
new_ltEs16(EQ, GT)
new_primEqNat0(Zero, Succ(x0))
new_esEs6(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_compare24(x0, x1, True, x2, x3)
new_primCmpInt(Neg(Zero), Pos(Zero))
new_primCmpInt(Pos(Zero), Neg(Zero))
new_lt8(x0, x1)
new_ltEs16(LT, EQ)
new_ltEs16(EQ, LT)
new_primMulInt(Pos(x0), Neg(x1))
new_primMulInt(Neg(x0), Pos(x1))
new_ltEs11(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs4(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs20(GT)
new_esEs22(x0, x1, ty_Integer)
new_esEs6(Right(x0), Right(x1), x2, ty_@0)
new_asAs(False, x0)
new_compare16(x0, x1, x2)
new_ltEs6(x0, x1, ty_Char)
new_ltEs6(x0, x1, ty_Double)
new_esEs8(x0, x1, ty_@0)
new_sr(Integer(x0), Integer(x1))
new_lt4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primCmpInt(Neg(Zero), Neg(Succ(x0)))
new_primPlusNat0(Succ(x0), x1)
new_esEs6(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_ltEs6(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(Nothing, Nothing, x0)
new_compare19(x0, x1, True, x2)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs6(Left(x0), Left(x1), ty_Int, x2)
new_compare110(x0, x1, False)
new_esEs8(x0, x1, app(ty_[], x2))
new_compare14(x0, x1, x2, x3, x4)
new_ltEs11(Just(x0), Just(x1), app(ty_Ratio, x2))
new_ltEs10(False, True)
new_esEs6(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_ltEs10(True, False)
new_esEs6(Left(x0), Left(x1), ty_Char, x2)
new_esEs5(Just(x0), Just(x1), ty_Ordering)
new_esEs27(x0, x1, ty_Integer)
new_compare12(x0, x1, False, x2, x3)
new_esEs17(True, False)
new_esEs17(False, True)
new_ltEs5(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_ltEs9(x0, x1, x2)
new_esEs6(Right(x0), Right(x1), x2, ty_Double)
new_esEs5(Just(x0), Just(x1), app(ty_[], x2))
new_ltEs11(Nothing, Nothing, x0)
new_primMulInt(Neg(x0), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_compare31(x0, x1, x2, x3)
new_lt19(x0, x1, ty_Char)
new_ltEs6(x0, x1, app(app(ty_Either, x2), x3))
new_ltEs6(x0, x1, ty_@0)
new_lt20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs17(True, True)
new_lt19(x0, x1, ty_@0)
new_compare33(x0, x1, app(ty_Maybe, x2))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_lt19(x0, x1, app(ty_[], x2))
new_lt4(x0, x1, app(ty_Ratio, x2))
new_ltEs6(x0, x1, app(app(ty_@2, x2), x3))
new_lt20(x0, x1, ty_Bool)
new_esEs8(x0, x1, ty_Char)
new_esEs27(x0, x1, ty_Ordering)
new_compare29(x0, x1, False)
new_compare23(x0, x1, False, x2, x3)
new_esEs22(x0, x1, ty_Ordering)
new_compare26(x0, x1, False, x2)
new_ltEs5(Right(x0), Right(x1), x2, ty_Integer)
new_primCmpNat0(Succ(x0), Zero)
new_esEs22(x0, x1, ty_@0)
new_not(LT)
new_compare30(x0, x1, x2, x3)
new_lt20(x0, x1, ty_Int)
new_compare25(x0, x1, False, x2, x3, x4)
new_esEs14(Char(x0), Char(x1))
new_lt4(x0, x1, ty_Double)
new_primCmpInt(Pos(Succ(x0)), Pos(x1))
new_esEs24(x0, x1, ty_Bool)
new_esEs6(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs9(x0, x1, app(ty_Maybe, x2))
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_compare20(vwx300, vwx400, False, cf) → new_ltEs0(vwx300, vwx400, cf)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3
- new_compare2(vwx300, vwx400, False, cc, cd) → new_ltEs(vwx300, vwx400, cc, cd)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 5 >= 4
- new_ltEs3(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), baf, bag, app(app(ty_@2, bah), bba)) → new_ltEs(vwx302, vwx402, bah, bba)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_ltEs3(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), baf, bag, app(ty_Maybe, bbb)) → new_ltEs0(vwx302, vwx402, bbb)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_ltEs3(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), baf, bag, app(app(app(ty_@3, bbf), bbg), bbh)) → new_ltEs3(vwx302, vwx402, bbf, bbg, bbh)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_lt0(vwx300, vwx400, cf) → new_compare20(vwx300, vwx400, new_esEs5(vwx300, vwx400, cf), cf)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 4
- new_lt1(vwx300, vwx400, cg, da) → new_compare21(vwx300, vwx400, new_esEs6(vwx300, vwx400, cg, da), cg, da)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 4, 4 >= 5
- new_ltEs(@2(vwx300, vwx301), @2(vwx400, vwx401), ba, app(app(ty_@2, bb), bc)) → new_ltEs(vwx301, vwx401, bb, bc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_ltEs(@2(vwx300, vwx301), @2(vwx400, vwx401), ba, app(ty_Maybe, bd)) → new_ltEs0(vwx301, vwx401, bd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_ltEs(@2(vwx300, vwx301), @2(vwx400, vwx401), ba, app(app(app(ty_@3, bh), ca), cb)) → new_ltEs3(vwx301, vwx401, bh, ca, cb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_ltEs(@2(vwx300, vwx301), @2(vwx400, vwx401), app(app(ty_@2, cc), cd), ce) → new_compare2(vwx300, vwx400, new_esEs4(vwx300, vwx400, cc, cd), cc, cd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 4, 3 > 5
- new_ltEs0(Just(vwx300), Just(vwx400), app(app(ty_@2, df), dg)) → new_ltEs(vwx300, vwx400, df, dg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_ltEs3(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), baf, bag, app(app(ty_Either, bbc), bbd)) → new_ltEs1(vwx302, vwx402, bbc, bbd)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_ltEs0(Just(vwx300), Just(vwx400), app(ty_Maybe, dh)) → new_ltEs0(vwx300, vwx400, dh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_ltEs(@2(vwx300, vwx301), @2(vwx400, vwx401), ba, app(app(ty_Either, be), bf)) → new_ltEs1(vwx301, vwx401, be, bf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_ltEs0(Just(vwx300), Just(vwx400), app(app(app(ty_@3, ed), ee), ef)) → new_ltEs3(vwx300, vwx400, ed, ee, ef)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_compare22(vwx300, vwx400, False, dc, dd, de) → new_ltEs3(vwx300, vwx400, dc, dd, de)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 5 >= 4, 6 >= 5
- new_ltEs0(Just(vwx300), Just(vwx400), app(app(ty_Either, ea), eb)) → new_ltEs1(vwx300, vwx400, ea, eb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_compare21(vwx300, vwx400, False, cg, da) → new_ltEs1(vwx300, vwx400, cg, da)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 5 >= 4
- new_ltEs0(Just(vwx300), Just(vwx400), app(ty_[], ec)) → new_ltEs2(vwx300, vwx400, ec)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_primCompAux(vwx300, vwx400, vwx49, app(app(app(ty_@3, bac), bad), bae)) → new_compare5(vwx300, vwx400, bac, bad, bae)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 > 3, 4 > 4, 4 > 5
- new_primCompAux(vwx300, vwx400, vwx49, app(ty_Maybe, hg)) → new_compare3(vwx300, vwx400, hg)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 > 3
- new_lt2(vwx300, vwx400, db) → new_compare(vwx300, vwx400, db)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3
- new_lt(vwx300, vwx400, cc, cd) → new_compare2(vwx300, vwx400, new_esEs4(vwx300, vwx400, cc, cd), cc, cd)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 4, 4 >= 5
- new_compare1(vwx300, vwx400, cc, cd) → new_compare2(vwx300, vwx400, new_esEs4(vwx300, vwx400, cc, cd), cc, cd)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 4, 4 >= 5
- new_ltEs(@2(vwx300, vwx301), @2(vwx400, vwx401), app(app(app(ty_@3, dc), dd), de), ce) → new_compare22(vwx300, vwx400, new_esEs7(vwx300, vwx400, dc, dd, de), dc, dd, de)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 4, 3 > 5, 3 > 6
- new_ltEs2(:(vwx300, vwx301), :(vwx400, vwx401), hd) → new_primCompAux(vwx300, vwx400, new_compare0(vwx301, vwx401, hd), hd)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 4
- new_ltEs2(:(vwx300, vwx301), :(vwx400, vwx401), hd) → new_compare(vwx301, vwx401, hd)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
- new_compare(:(vwx300, vwx301), :(vwx400, vwx401), hd) → new_primCompAux(vwx300, vwx400, new_compare0(vwx301, vwx401, hd), hd)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 4
- new_compare(:(vwx300, vwx301), :(vwx400, vwx401), hd) → new_compare(vwx301, vwx401, hd)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
- new_ltEs(@2(vwx300, vwx301), @2(vwx400, vwx401), app(app(ty_Either, cg), da), ce) → new_compare21(vwx300, vwx400, new_esEs6(vwx300, vwx400, cg, da), cg, da)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 4, 3 > 5
- new_compare4(vwx300, vwx400, cg, da) → new_compare21(vwx300, vwx400, new_esEs6(vwx300, vwx400, cg, da), cg, da)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 4, 4 >= 5
- new_ltEs3(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), baf, bag, app(ty_[], bbe)) → new_ltEs2(vwx302, vwx402, bbe)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_ltEs(@2(vwx300, vwx301), @2(vwx400, vwx401), ba, app(ty_[], bg)) → new_ltEs2(vwx301, vwx401, bg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_compare3(vwx300, vwx400, cf) → new_compare20(vwx300, vwx400, new_esEs5(vwx300, vwx400, cf), cf)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 4
- new_compare5(vwx300, vwx400, dc, dd, de) → new_compare22(vwx300, vwx400, new_esEs7(vwx300, vwx400, dc, dd, de), dc, dd, de)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 4, 4 >= 5, 5 >= 6
- new_lt3(vwx300, vwx400, dc, dd, de) → new_compare22(vwx300, vwx400, new_esEs7(vwx300, vwx400, dc, dd, de), dc, dd, de)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 4, 4 >= 5, 5 >= 6
- new_ltEs(@2(vwx300, vwx301), @2(vwx400, vwx401), app(ty_[], db), ce) → new_compare(vwx300, vwx400, db)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_ltEs(@2(vwx300, vwx301), @2(vwx400, vwx401), app(ty_Maybe, cf), ce) → new_compare20(vwx300, vwx400, new_esEs5(vwx300, vwx400, cf), cf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 4
- new_primCompAux(vwx300, vwx400, vwx49, app(ty_[], bab)) → new_compare(vwx300, vwx400, bab)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 > 3
- new_primCompAux(vwx300, vwx400, vwx49, app(app(ty_Either, hh), baa)) → new_compare4(vwx300, vwx400, hh, baa)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 > 3, 4 > 4
- new_primCompAux(vwx300, vwx400, vwx49, app(app(ty_@2, he), hf)) → new_compare1(vwx300, vwx400, he, hf)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 > 3, 4 > 4
- new_ltEs1(Left(vwx300), Left(vwx400), app(app(ty_@2, eg), eh), fa) → new_ltEs(vwx300, vwx400, eg, eh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_ltEs1(Right(vwx300), Right(vwx400), gb, app(app(ty_@2, gc), gd)) → new_ltEs(vwx300, vwx400, gc, gd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_ltEs3(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), app(app(ty_@2, bdc), bdd), bag, bcc) → new_lt(vwx300, vwx400, bdc, bdd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_ltEs3(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), baf, app(app(ty_@2, bca), bcb), bcc) → new_lt(vwx301, vwx401, bca, bcb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_ltEs3(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), app(app(app(ty_@3, bea), beb), bec), bag, bcc) → new_lt3(vwx300, vwx400, bea, beb, bec)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_ltEs3(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), baf, app(app(app(ty_@3, bch), bda), bdb), bcc) → new_lt3(vwx301, vwx401, bch, bda, bdb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_ltEs3(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), baf, app(app(ty_Either, bce), bcf), bcc) → new_lt1(vwx301, vwx401, bce, bcf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_ltEs3(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), app(app(ty_Either, bdf), bdg), bag, bcc) → new_lt1(vwx300, vwx400, bdf, bdg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_ltEs3(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), baf, app(ty_[], bcg), bcc) → new_lt2(vwx301, vwx401, bcg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_ltEs3(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), app(ty_[], bdh), bag, bcc) → new_lt2(vwx300, vwx400, bdh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_ltEs3(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), baf, app(ty_Maybe, bcd), bcc) → new_lt0(vwx301, vwx401, bcd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_ltEs3(@3(vwx300, vwx301, vwx302), @3(vwx400, vwx401, vwx402), app(ty_Maybe, bde), bag, bcc) → new_lt0(vwx300, vwx400, bde)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_ltEs1(Left(vwx300), Left(vwx400), app(ty_Maybe, fb), fa) → new_ltEs0(vwx300, vwx400, fb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_ltEs1(Right(vwx300), Right(vwx400), gb, app(ty_Maybe, ge)) → new_ltEs0(vwx300, vwx400, ge)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_ltEs1(Right(vwx300), Right(vwx400), gb, app(app(app(ty_@3, ha), hb), hc)) → new_ltEs3(vwx300, vwx400, ha, hb, hc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_ltEs1(Left(vwx300), Left(vwx400), app(app(app(ty_@3, fg), fh), ga), fa) → new_ltEs3(vwx300, vwx400, fg, fh, ga)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_ltEs1(Left(vwx300), Left(vwx400), app(app(ty_Either, fc), fd), fa) → new_ltEs1(vwx300, vwx400, fc, fd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_ltEs1(Right(vwx300), Right(vwx400), gb, app(app(ty_Either, gf), gg)) → new_ltEs1(vwx300, vwx400, gf, gg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_ltEs1(Left(vwx300), Left(vwx400), app(ty_[], ff), fa) → new_ltEs2(vwx300, vwx400, ff)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_ltEs1(Right(vwx300), Right(vwx400), gb, app(ty_[], gh)) → new_ltEs2(vwx300, vwx400, gh)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3